Proof of Theorem lcfl6
Step | Hyp | Ref
| Expression |
1 | | df-ne 2782 |
. . . . 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 2610 |
. . . . . . . 8
⊢
(1r‘𝑆) = (1r‘𝑆) |
9 | | lcfl6.f |
. . . . . . . 8
⊢ 𝐹 = (LFnl‘𝑈) |
10 | | lcfl6.l |
. . . . . . . 8
⊢ 𝐿 = (LKer‘𝑈) |
11 | | lcfl6.k |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
12 | 11 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
13 | | lcfl6.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
14 | 13 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) → 𝐺 ∈ 𝐹) |
15 | | lcfl6.c |
. . . . . . . . . . . . . 14
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
16 | 2, 3, 4, 5, 9, 10,
15, 11, 13 | lcfl2 35800 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉))) |
17 | 16 | biimpa 500 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → (( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉)) |
18 | 17 | orcomd 402 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → ((𝐿‘𝐺) = 𝑉 ∨ ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉)) |
19 | 18 | ord 391 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → (¬ (𝐿‘𝐺) = 𝑉 → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉)) |
20 | 1, 19 | syl5bi 231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → ((𝐿‘𝐺) ≠ 𝑉 → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉)) |
21 | 20 | imp 444 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉) |
22 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 12, 14, 21 | dochkr1 35785 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) → ∃𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })(𝐺‘𝑥) = (1r‘𝑆)) |
23 | 2, 4, 11 | dvhlmod 35417 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ∈ LMod) |
24 | 5, 9, 10, 23, 13 | lkrssv 33401 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿‘𝐺) ⊆ 𝑉) |
25 | 2, 4, 5, 3 | dochssv 35662 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘𝐺) ⊆ 𝑉) → ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑉) |
26 | 11, 24, 25 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑉) |
27 | 26 | ssdifd 3708 |
. . . . . . . . . . . 12
⊢ (𝜑 → (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ⊆ (𝑉 ∖ { 0 })) |
28 | 27 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ⊆ (𝑉 ∖ { 0 })) |
29 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → 𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) |
30 | 28, 29 | sseldd 3569 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → 𝑥 ∈ (𝑉 ∖ { 0 })) |
31 | | lcfl6.a |
. . . . . . . . . . 11
⊢ + =
(+g‘𝑈) |
32 | | lcfl6.t |
. . . . . . . . . . 11
⊢ · = (
·𝑠 ‘𝑈) |
33 | | lcfl6.r |
. . . . . . . . . . 11
⊢ 𝑅 = (Base‘𝑆) |
34 | 11 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
35 | 13 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → 𝐺 ∈ 𝐹) |
36 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → (𝐺‘𝑥) = (1r‘𝑆)) |
37 | 2, 3, 4, 5, 31, 32, 6, 8, 33, 7, 9, 10, 34, 35, 29, 36 | lcfl6lem 35805 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) |
38 | 30, 37 | jca 553 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) ∧ (𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆))) → (𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))) |
39 | 38 | ex 449 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) → ((𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 }) ∧ (𝐺‘𝑥) = (1r‘𝑆)) → (𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))))) |
40 | 39 | reximdv2 2997 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) → (∃𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })(𝐺‘𝑥) = (1r‘𝑆) → ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))) |
41 | 22, 40 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐺 ∈ 𝐶) ∧ (𝐿‘𝐺) ≠ 𝑉) → ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) |
42 | 41 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → ((𝐿‘𝐺) ≠ 𝑉 → ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))) |
43 | 1, 42 | syl5bir 232 |
. . . 4
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → (¬ (𝐿‘𝐺) = 𝑉 → ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))) |
44 | 43 | orrd 392 |
. . 3
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐶) → ((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))) |
45 | 44 | ex 449 |
. 2
⊢ (𝜑 → (𝐺 ∈ 𝐶 → ((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))))) |
46 | | olc 398 |
. . . 4
⊢ ((𝐿‘𝐺) = 𝑉 → (( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉)) |
47 | 46, 16 | syl5ibr 235 |
. . 3
⊢ (𝜑 → ((𝐿‘𝐺) = 𝑉 → 𝐺 ∈ 𝐶)) |
48 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
49 | | eldifi 3694 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑉 ∖ { 0 }) → 𝑥 ∈ 𝑉) |
50 | 49 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → 𝑥 ∈ 𝑉) |
51 | 50 | snssd 4281 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → {𝑥} ⊆ 𝑉) |
52 | | eqid 2610 |
. . . . . . . . . 10
⊢
((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊) |
53 | 2, 52, 4, 5, 3 | dochcl 35660 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑥} ⊆ 𝑉) → ( ⊥ ‘{𝑥}) ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
54 | 48, 51, 53 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → ( ⊥
‘{𝑥}) ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
55 | 2, 52, 3 | dochoc 35674 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘{𝑥}) ∈ ran
((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘( ⊥
‘( ⊥ ‘{𝑥}))) = ( ⊥ ‘{𝑥})) |
56 | 48, 54, 55 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → ( ⊥
‘( ⊥ ‘( ⊥
‘{𝑥}))) = ( ⊥
‘{𝑥})) |
57 | 56 | 3adant3 1074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → ( ⊥ ‘( ⊥
‘( ⊥ ‘{𝑥}))) = ( ⊥ ‘{𝑥})) |
58 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) |
59 | 58 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → (𝐿‘𝐺) = (𝐿‘(𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))) |
60 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))) = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))) |
61 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → 𝑥 ∈ (𝑉 ∖ { 0 })) |
62 | 2, 3, 4, 5, 7, 31,
32, 10, 6, 33, 60, 48, 61 | dochsnkr2 35780 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → (𝐿‘(𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) = ( ⊥ ‘{𝑥})) |
63 | 62 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → (𝐿‘(𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) = ( ⊥ ‘{𝑥})) |
64 | 59, 63 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → (𝐿‘𝐺) = ( ⊥ ‘{𝑥})) |
65 | 64 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → ( ⊥ ‘(𝐿‘𝐺)) = ( ⊥ ‘( ⊥
‘{𝑥}))) |
66 | 65 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = ( ⊥ ‘( ⊥
‘( ⊥ ‘{𝑥})))) |
67 | 57, 66, 64 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺)) |
68 | 13 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → 𝐺 ∈ 𝐹) |
69 | 15, 68 | lcfl1 35799 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → (𝐺 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺))) |
70 | 67, 69 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 }) ∧ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → 𝐺 ∈ 𝐶) |
71 | 70 | rexlimdv3a 3015 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))) → 𝐺 ∈ 𝐶)) |
72 | 47, 71 | jaod 394 |
. 2
⊢ (𝜑 → (((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) → 𝐺 ∈ 𝐶)) |
73 | 45, 72 | impbid 201 |
1
⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))))) |