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 39120 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ LMod) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → 𝑈 ∈ LMod) |
6 | | lcfl8.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑈) |
7 | | eqid 2740 |
. . . . . . 7
⊢
(LSpan‘𝑈) =
(LSpan‘𝑈) |
8 | | eqid 2740 |
. . . . . . 7
⊢
(LSAtoms‘𝑈) =
(LSAtoms‘𝑈) |
9 | 6, 7, 8 | islsati 37004 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ ( ⊥
‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) → ∃𝑥 ∈ 𝑉 ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) |
10 | 5, 9 | sylan 580 |
. . . . 5
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) → ∃𝑥 ∈ 𝑉 ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) |
11 | | simpr 485 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) |
12 | 11 | fveq2d 6775 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = ( ⊥
‘((LSpan‘𝑈)‘{𝑥}))) |
13 | | simp-4r 781 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → 𝐺 ∈ 𝐶) |
14 | | lcfl8.c |
. . . . . . . . . 10
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
15 | | lcfl8.g |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
16 | 15 | ad4antr 729 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → 𝐺 ∈ 𝐹) |
17 | 14, 16 | lcfl1 39502 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → (𝐺 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺))) |
18 | 13, 17 | mpbid 231 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺)) |
19 | | lcfl8.o |
. . . . . . . . 9
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
20 | 3 | ad4antr 729 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
21 | | simplr 766 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → 𝑥 ∈ 𝑉) |
22 | 21 | snssd 4748 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → {𝑥} ⊆ 𝑉) |
23 | 1, 2, 19, 6, 7, 20, 22 | dochocsp 39389 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → ( ⊥
‘((LSpan‘𝑈)‘{𝑥})) = ( ⊥ ‘{𝑥})) |
24 | 12, 18, 23 | 3eqtr3d 2788 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) ∧ ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥})) → (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
25 | 24 | ex 413 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) ∧ 𝑥 ∈ 𝑉) → (( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥}) → (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) |
26 | 25 | reximdva 3205 |
. . . . 5
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) → (∃𝑥 ∈ 𝑉 ( ⊥ ‘(𝐿‘𝐺)) = ((LSpan‘𝑈)‘{𝑥}) → ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) |
27 | 10, 26 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) → ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
28 | 5 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → 𝑈 ∈ LMod) |
29 | | eqid 2740 |
. . . . . . 7
⊢
(0g‘𝑈) = (0g‘𝑈) |
30 | 6, 29 | lmod0vcl 20150 |
. . . . . 6
⊢ (𝑈 ∈ LMod →
(0g‘𝑈)
∈ 𝑉) |
31 | 28, 30 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → (0g‘𝑈) ∈ 𝑉) |
32 | | simpr 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → (𝐿‘𝐺) = 𝑉) |
33 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
34 | 33 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
35 | 1, 2, 19, 6, 29 | doch0 39368 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( ⊥
‘{(0g‘𝑈)}) = 𝑉) |
36 | 34, 35 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → ( ⊥
‘{(0g‘𝑈)}) = 𝑉) |
37 | 32, 36 | eqtr4d 2783 |
. . . . 5
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → (𝐿‘𝐺) = ( ⊥
‘{(0g‘𝑈)})) |
38 | | sneq 4577 |
. . . . . . 7
⊢ (𝑥 = (0g‘𝑈) → {𝑥} = {(0g‘𝑈)}) |
39 | 38 | fveq2d 6775 |
. . . . . 6
⊢ (𝑥 = (0g‘𝑈) → ( ⊥ ‘{𝑥}) = ( ⊥
‘{(0g‘𝑈)})) |
40 | 39 | rspceeqv 3576 |
. . . . 5
⊢
(((0g‘𝑈) ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥
‘{(0g‘𝑈)})) → ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
41 | 31, 37, 40 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) = 𝑉) → ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
42 | | lcfl8.f |
. . . . . 6
⊢ 𝐹 = (LFnl‘𝑈) |
43 | | lcfl8.l |
. . . . . 6
⊢ 𝐿 = (LKer‘𝑈) |
44 | 1, 19, 2, 6, 8, 42,
43, 14, 3, 15 | lcfl3 39504 |
. . . . 5
⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈) ∨ (𝐿‘𝐺) = 𝑉))) |
45 | 44 | biimpa 477 |
. . . 4
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → (( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈) ∨ (𝐿‘𝐺) = 𝑉)) |
46 | 27, 41, 45 | mpjaodan 956 |
. . 3
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
47 | 46 | ex 413 |
. 2
⊢ (𝜑 → (𝐺 ∈ 𝐶 → ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) |
48 | 3 | 3ad2ant1 1132 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
49 | | simp2 1136 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → 𝑥 ∈ 𝑉) |
50 | 49 | snssd 4748 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → {𝑥} ⊆ 𝑉) |
51 | | eqid 2740 |
. . . . . . . 8
⊢
((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊) |
52 | 1, 51, 2, 6, 19 | dochcl 39363 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑥} ⊆ 𝑉) → ( ⊥ ‘{𝑥}) ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
53 | 48, 50, 52 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → ( ⊥ ‘{𝑥}) ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
54 | 1, 51, 19 | dochoc 39377 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘{𝑥}) ∈ ran
((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘( ⊥
‘( ⊥ ‘{𝑥}))) = ( ⊥ ‘{𝑥})) |
55 | 48, 53, 54 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → ( ⊥ ‘( ⊥
‘( ⊥ ‘{𝑥}))) = ( ⊥ ‘{𝑥})) |
56 | | simp3 1137 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
57 | 56 | fveq2d 6775 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → ( ⊥ ‘(𝐿‘𝐺)) = ( ⊥ ‘( ⊥
‘{𝑥}))) |
58 | 57 | fveq2d 6775 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = ( ⊥ ‘( ⊥
‘( ⊥ ‘{𝑥})))) |
59 | 55, 58, 56 | 3eqtr4d 2790 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺)) |
60 | 59 | rexlimdv3a 3217 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺))) |
61 | 14, 15 | lcfl1 39502 |
. . 3
⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺))) |
62 | 60, 61 | sylibrd 258 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}) → 𝐺 ∈ 𝐶)) |
63 | 47, 62 | impbid 211 |
1
⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) |