Proof of Theorem lcfl8
Step | Hyp | Ref
| Expression |
1 | | lcfl8.h |
. . . . . . . 8
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | lcfl8.u |
. . . . . . . 8
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
3 | | lcfl8.k |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
4 | 1, 2, 3 | dvhlmod 35417 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ LMod) |
5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → 𝑈 ∈ LMod) |
6 | | lcfl8.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑈) |
7 | | eqid 2610 |
. . . . . . 7
⊢
(LSpan‘𝑈) =
(LSpan‘𝑈) |
8 | | eqid 2610 |
. . . . . . 7
⊢
(LSAtoms‘𝑈) =
(LSAtoms‘𝑈) |
9 | 6, 7, 8 | islsati 33299 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ ( ⊥
‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) → ∃𝑥 ∈ 𝑉 ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) |
10 | 5, 9 | sylan 487 |
. . . . 5
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) → ∃𝑥 ∈ 𝑉 ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) |
11 | | simpr 476 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) |
12 | 11 | fveq2d 6107 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = ( ⊥
‘((LSpan‘𝑈)‘{𝑥}))) |
13 | | simp-4r 803 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → 𝐺 ∈ 𝐶) |
14 | | lcfl8.c |
. . . . . . . . . 10
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
15 | | lcfl8.g |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
16 | 15 | ad4antr 764 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → 𝐺 ∈ 𝐹) |
17 | 14, 16 | lcfl1 35799 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → (𝐺 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺))) |
18 | 13, 17 | mpbid 221 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺)) |
19 | | lcfl8.o |
. . . . . . . . 9
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
20 | 3 | ad4antr 764 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
21 | | simplr 788 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → 𝑥 ∈ 𝑉) |
22 | 21 | snssd 4281 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → {𝑥} ⊆ 𝑉) |
23 | 1, 2, 19, 6, 7, 20, 22 | dochocsp 35686 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → ( ⊥
‘((LSpan‘𝑈)‘{𝑥})) = ( ⊥ ‘{𝑥})) |
24 | 12, 18, 23 | 3eqtr3d 2652 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
25 | 24 | ex 449 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) → (( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥}) → (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) |
26 | 25 | reximdva 3000 |
. . . . 5
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) → (∃𝑥 ∈ 𝑉 ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥}) → ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) |
27 | 10, 26 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) → ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
28 | 5 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → 𝑈 ∈ LMod) |
29 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑈) = (0g‘𝑈) |
30 | 6, 29 | lmod0vcl 18715 |
. . . . . 6
⊢ (𝑈 ∈ LMod →
(0g‘𝑈)
∈ 𝑉) |
31 | 28, 30 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → (0g‘𝑈) ∈ 𝑉) |
32 | | simpr 476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → (𝐿‘𝐺) = 𝑉) |
33 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
34 | 33 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
35 | 1, 2, 19, 6, 29 | doch0 35665 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( ⊥
‘{(0g‘𝑈)}) = 𝑉) |
36 | 34, 35 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → ( ⊥
‘{(0g‘𝑈)}) = 𝑉) |
37 | 32, 36 | eqtr4d 2647 |
. . . . 5
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → (𝐿‘𝐺) = ( ⊥
‘{(0g‘𝑈)})) |
38 | | sneq 4135 |
. . . . . . . 8
⊢ (𝑥 = (0g‘𝑈) → {𝑥} = {(0g‘𝑈)}) |
39 | 38 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = (0g‘𝑈) → ( ⊥ ‘{𝑥}) = ( ⊥
‘{(0g‘𝑈)})) |
40 | 39 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑥 = (0g‘𝑈) → ((𝐿‘𝐺) = ( ⊥ ‘{𝑥}) ↔ (𝐿‘𝐺) = ( ⊥
‘{(0g‘𝑈)}))) |
41 | 40 | rspcev 3282 |
. . . . 5
⊢
(((0g‘𝑈) ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥
‘{(0g‘𝑈)})) → ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
42 | 31, 37, 41 | syl2anc 691 |
. . . 4
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
43 | | lcfl8.f |
. . . . . 6
⊢ 𝐹 = (LFnl‘𝑈) |
44 | | lcfl8.l |
. . . . . 6
⊢ 𝐿 = (LKer‘𝑈) |
45 | 1, 19, 2, 6, 8, 43,
44, 14, 3, 15 | lcfl3 35801 |
. . . . 5
⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈) ∨ (𝐿‘𝐺) = 𝑉))) |
46 | 45 | biimpa 500 |
. . . 4
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → (( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈) ∨ (𝐿‘𝐺) = 𝑉)) |
47 | 27, 42, 46 | mpjaodan 823 |
. . 3
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
48 | 47 | ex 449 |
. 2
⊢ (𝜑 → (𝐺 ∈ 𝐶 → ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) |
49 | 3 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
50 | | simp2 1055 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → 𝑥 ∈ 𝑉) |
51 | 50 | snssd 4281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → {𝑥} ⊆ 𝑉) |
52 | | eqid 2610 |
. . . . . . . 8
⊢
((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊) |
53 | 1, 52, 2, 6, 19 | dochcl 35660 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑥} ⊆ 𝑉) → ( ⊥ ‘{𝑥}) ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
54 | 49, 51, 53 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → ( ⊥ ‘{𝑥}) ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
55 | 1, 52, 19 | dochoc 35674 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘{𝑥}) ∈ ran
((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘( ⊥
‘( ⊥ ‘{𝑥}))) = ( ⊥ ‘{𝑥})) |
56 | 49, 54, 55 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → ( ⊥ ‘( ⊥
‘( ⊥ ‘{𝑥}))) = ( ⊥ ‘{𝑥})) |
57 | | simp3 1056 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
58 | 57 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → ( ⊥ ‘(𝐿‘𝐺)) = ( ⊥ ‘( ⊥
‘{𝑥}))) |
59 | 58 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = ( ⊥ ‘( ⊥
‘( ⊥ ‘{𝑥})))) |
60 | 56, 59, 57 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺)) |
61 | 60 | rexlimdv3a 3015 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺))) |
62 | 14, 15 | lcfl1 35799 |
. . 3
⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺))) |
63 | 61, 62 | sylibrd 248 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}) → 𝐺 ∈ 𝐶)) |
64 | 48, 63 | impbid 201 |
1
⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) |