Proof of Theorem lcfl6
Step | Hyp | Ref
| Expression |
1 | | df-ne 2941 |
. . . . 5
⊢ ((𝐿‘𝐺) ≠ 𝑉 ↔ ¬ (𝐿‘𝐺) = 𝑉) |
2 | | lcfl6.h |
. . . . . . . 8
⊢ 𝐻 = (LHyp‘𝐾) |
3 | | lcfl6.o |
. . . . . . . 8
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
4 | | lcfl6.u |
. . . . . . . 8
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
5 | | lcfl6.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝑈) |
6 | | lcfl6.s |
. . . . . . . 8
⊢ 𝑆 = (Scalar‘𝑈) |
7 | | lcfl6.z |
. . . . . . . 8
⊢ 0 =
(0g‘𝑈) |
8 | | eqid 2737 |
. . . . . . . 8
⊢
(1r‘𝑆) = (1r‘𝑆) |
9 | | lcfl6.f |
. . . . . . . 8
⊢ 𝐹 = (LFnl‘𝑈) |
10 | | lcfl6.l |
. . . . . . . 8
⊢ 𝐿 = (LKer‘𝑈) |
11 | | lcfl6.k |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
12 | 11 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
13 | | lcfl6.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
14 | 13 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) → 𝐺 ∈ 𝐹) |
15 | | lcfl6.c |
. . . . . . . . . . . . . 14
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
16 | 2, 3, 4, 5, 9, 10,
15, 11, 13 | lcfl2 39244 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉))) |
17 | 16 | biimpa 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → (( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉)) |
18 | 17 | orcomd 871 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → ((𝐿‘𝐺) = 𝑉 ∨ ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉)) |
19 | 18 | ord 864 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → (¬ (𝐿‘𝐺) = 𝑉 → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉)) |
20 | 1, 19 | syl5bi 245 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → ((𝐿‘𝐺) ≠ 𝑉 → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉)) |
21 | 20 | imp 410 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉) |
22 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 12, 14, 21 | dochkr1 39229 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) → ∃𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })(𝐺‘𝑥) = (1r‘𝑆)) |
23 | 2, 4, 11 | dvhlmod 38861 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ LMod) |
24 | 5, 9, 10, 23, 13 | lkrssv 36847 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐿‘𝐺) ⊆ 𝑉) |
25 | 2, 4, 5, 3 | dochssv 39106 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘𝐺) ⊆ 𝑉) → ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑉) |
26 | 11, 24, 25 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑉) |
27 | 26 | ssdifd 4055 |
. . . . . . . . 9
⊢ (𝜑 → (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ⊆ (𝑉 ∖ { 0 })) |
28 | 27 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ⊆ (𝑉 ∖ { 0 })) |
29 | | simprl 771 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → 𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) |
30 | 28, 29 | sseldd 3902 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → 𝑥 ∈ (𝑉 ∖ { 0 })) |
31 | | lcfl6.a |
. . . . . . . 8
⊢ + =
(+g‘𝑈) |
32 | | lcfl6.t |
. . . . . . . 8
⊢ · = (
·𝑠 ‘𝑈) |
33 | | lcfl6.r |
. . . . . . . 8
⊢ 𝑅 = (Base‘𝑆) |
34 | 11 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
35 | 13 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → 𝐺 ∈ 𝐹) |
36 | | simprr 773 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → (𝐺‘𝑥) = (1r‘𝑆)) |
37 | 2, 3, 4, 5, 31, 32, 6, 8, 33, 7, 9, 10, 34, 35, 29, 36 | lcfl6lem 39249 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) |
38 | 22, 30, 37 | reximssdv 3195 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) → ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) |
39 | 38 | ex 416 |
. . . . 5
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → ((𝐿‘𝐺) ≠ 𝑉 → ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))) |
40 | 1, 39 | syl5bir 246 |
. . . 4
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → (¬ (𝐿‘𝐺) = 𝑉 → ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))) |
41 | 40 | orrd 863 |
. . 3
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → ((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))) |
42 | 41 | ex 416 |
. 2
⊢ (𝜑 → (𝐺 ∈ 𝐶 → ((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))))) |
43 | | olc 868 |
. . . 4
⊢ ((𝐿‘𝐺) = 𝑉 → (( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉)) |
44 | 43, 16 | syl5ibr 249 |
. . 3
⊢ (𝜑 → ((𝐿‘𝐺) = 𝑉 → 𝐺 ∈ 𝐶)) |
45 | 11 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
46 | | eldifi 4041 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑉 ∖ { 0 }) → 𝑥 ∈ 𝑉) |
47 | 46 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → 𝑥 ∈ 𝑉) |
48 | 47 | snssd 4722 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → {𝑥} ⊆ 𝑉) |
49 | | eqid 2737 |
. . . . . . . . . 10
⊢
((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊) |
50 | 2, 49, 4, 5, 3 | dochcl 39104 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑥} ⊆ 𝑉) → ( ⊥ ‘{𝑥}) ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
51 | 45, 48, 50 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → ( ⊥
‘{𝑥}) ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
52 | 2, 49, 3 | dochoc 39118 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘{𝑥}) ∈ ran
((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘( ⊥
‘( ⊥ ‘{𝑥}))) = ( ⊥ ‘{𝑥})) |
53 | 45, 51, 52 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → ( ⊥
‘( ⊥ ‘( ⊥
‘{𝑥}))) = ( ⊥
‘{𝑥})) |
54 | 53 | 3adant3 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → ( ⊥ ‘( ⊥
‘( ⊥ ‘{𝑥}))) = ( ⊥ ‘{𝑥})) |
55 | | simp3 1140 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) |
56 | 55 | fveq2d 6721 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → (𝐿‘𝐺) = (𝐿‘(𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))) |
57 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))) = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))) |
58 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → 𝑥 ∈ (𝑉 ∖ { 0 })) |
59 | 2, 3, 4, 5, 7, 31,
32, 10, 6, 33, 57, 45, 58 | dochsnkr2 39224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → (𝐿‘(𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) = ( ⊥ ‘{𝑥})) |
60 | 59 | 3adant3 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → (𝐿‘(𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) = ( ⊥ ‘{𝑥})) |
61 | 56, 60 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
62 | 61 | fveq2d 6721 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → ( ⊥ ‘(𝐿‘𝐺)) = ( ⊥ ‘( ⊥
‘{𝑥}))) |
63 | 62 | fveq2d 6721 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = ( ⊥ ‘( ⊥
‘( ⊥ ‘{𝑥})))) |
64 | 54, 63, 61 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺)) |
65 | 13 | 3ad2ant1 1135 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → 𝐺 ∈ 𝐹) |
66 | 15, 65 | lcfl1 39243 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → (𝐺 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺))) |
67 | 64, 66 | mpbird 260 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → 𝐺 ∈ 𝐶) |
68 | 67 | rexlimdv3a 3205 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))) → 𝐺 ∈ 𝐶)) |
69 | 44, 68 | jaod 859 |
. 2
⊢ (𝜑 → (((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → 𝐺 ∈ 𝐶)) |
70 | 42, 69 | impbid 215 |
1
⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))))) |