Step | Hyp | Ref
| Expression |
1 | | nne 2786 |
. . . . . . 7
⊢ (¬
(𝐺‘𝑧) ≠ 0 ↔ (𝐺‘𝑧) = 0 ) |
2 | 1 | ralbii 2963 |
. . . . . 6
⊢
(∀𝑧 ∈
𝑉 ¬ (𝐺‘𝑧) ≠ 0 ↔ ∀𝑧 ∈ 𝑉 (𝐺‘𝑧) = 0 ) |
3 | | lfl1.d |
. . . . . . . . . 10
⊢ 𝐷 = (Scalar‘𝑊) |
4 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝐷) =
(Base‘𝐷) |
5 | | lfl1.v |
. . . . . . . . . 10
⊢ 𝑉 = (Base‘𝑊) |
6 | | lfl1.f |
. . . . . . . . . 10
⊢ 𝐹 = (LFnl‘𝑊) |
7 | 3, 4, 5, 6 | lflf 33368 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → 𝐺:𝑉⟶(Base‘𝐷)) |
8 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐺:𝑉⟶(Base‘𝐷) → 𝐺 Fn 𝑉) |
9 | 7, 8 | syl 17 |
. . . . . . . 8
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → 𝐺 Fn 𝑉) |
10 | | fconstfv 6381 |
. . . . . . . . 9
⊢ (𝐺:𝑉⟶{ 0 } ↔ (𝐺 Fn 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝐺‘𝑧) = 0 )) |
11 | 10 | simplbi2 653 |
. . . . . . . 8
⊢ (𝐺 Fn 𝑉 → (∀𝑧 ∈ 𝑉 (𝐺‘𝑧) = 0 → 𝐺:𝑉⟶{ 0 })) |
12 | 9, 11 | syl 17 |
. . . . . . 7
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → (∀𝑧 ∈ 𝑉 (𝐺‘𝑧) = 0 → 𝐺:𝑉⟶{ 0 })) |
13 | | lfl1.o |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐷) |
14 | | fvex 6113 |
. . . . . . . . 9
⊢
(0g‘𝐷) ∈ V |
15 | 13, 14 | eqeltri 2684 |
. . . . . . . 8
⊢ 0 ∈
V |
16 | 15 | fconst2 6375 |
. . . . . . 7
⊢ (𝐺:𝑉⟶{ 0 } ↔ 𝐺 = (𝑉 × { 0 })) |
17 | 12, 16 | syl6ib 240 |
. . . . . 6
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → (∀𝑧 ∈ 𝑉 (𝐺‘𝑧) = 0 → 𝐺 = (𝑉 × { 0 }))) |
18 | 2, 17 | syl5bi 231 |
. . . . 5
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → (∀𝑧 ∈ 𝑉 ¬ (𝐺‘𝑧) ≠ 0 → 𝐺 = (𝑉 × { 0 }))) |
19 | 18 | necon3ad 2795 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → (𝐺 ≠ (𝑉 × { 0 }) → ¬
∀𝑧 ∈ 𝑉 ¬ (𝐺‘𝑧) ≠ 0 )) |
20 | | dfrex2 2979 |
. . . 4
⊢
(∃𝑧 ∈
𝑉 (𝐺‘𝑧) ≠ 0 ↔ ¬ ∀𝑧 ∈ 𝑉 ¬ (𝐺‘𝑧) ≠ 0 ) |
21 | 19, 20 | syl6ibr 241 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → (𝐺 ≠ (𝑉 × { 0 }) → ∃𝑧 ∈ 𝑉 (𝐺‘𝑧) ≠ 0 )) |
22 | 21 | 3impia 1253 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × { 0 })) → ∃𝑧 ∈ 𝑉 (𝐺‘𝑧) ≠ 0 ) |
23 | | simp1l 1078 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) → 𝑊 ∈ LVec) |
24 | | lveclmod 18927 |
. . . . . . 7
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) → 𝑊 ∈ LMod) |
26 | 3 | lvecdrng 18926 |
. . . . . . . 8
⊢ (𝑊 ∈ LVec → 𝐷 ∈
DivRing) |
27 | 23, 26 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) → 𝐷 ∈ DivRing) |
28 | | simp1r 1079 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) → 𝐺 ∈ 𝐹) |
29 | | simp2 1055 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) → 𝑧 ∈ 𝑉) |
30 | 3, 4, 5, 6 | lflcl 33369 |
. . . . . . . 8
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉) → (𝐺‘𝑧) ∈ (Base‘𝐷)) |
31 | 23, 28, 29, 30 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) → (𝐺‘𝑧) ∈ (Base‘𝐷)) |
32 | | simp3 1056 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) → (𝐺‘𝑧) ≠ 0 ) |
33 | | eqid 2610 |
. . . . . . . 8
⊢
(invr‘𝐷) = (invr‘𝐷) |
34 | 4, 13, 33 | drnginvrcl 18587 |
. . . . . . 7
⊢ ((𝐷 ∈ DivRing ∧ (𝐺‘𝑧) ∈ (Base‘𝐷) ∧ (𝐺‘𝑧) ≠ 0 ) →
((invr‘𝐷)‘(𝐺‘𝑧)) ∈ (Base‘𝐷)) |
35 | 27, 31, 32, 34 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) →
((invr‘𝐷)‘(𝐺‘𝑧)) ∈ (Base‘𝐷)) |
36 | | eqid 2610 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
37 | 5, 3, 36, 4 | lmodvscl 18703 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧
((invr‘𝐷)‘(𝐺‘𝑧)) ∈ (Base‘𝐷) ∧ 𝑧 ∈ 𝑉) → (((invr‘𝐷)‘(𝐺‘𝑧))( ·𝑠
‘𝑊)𝑧) ∈ 𝑉) |
38 | 25, 35, 29, 37 | syl3anc 1318 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) →
(((invr‘𝐷)‘(𝐺‘𝑧))( ·𝑠
‘𝑊)𝑧) ∈ 𝑉) |
39 | | eqid 2610 |
. . . . . . . 8
⊢
(.r‘𝐷) = (.r‘𝐷) |
40 | 3, 4, 39, 5, 36, 6 | lflmul 33373 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (((invr‘𝐷)‘(𝐺‘𝑧)) ∈ (Base‘𝐷) ∧ 𝑧 ∈ 𝑉)) → (𝐺‘(((invr‘𝐷)‘(𝐺‘𝑧))( ·𝑠
‘𝑊)𝑧)) = (((invr‘𝐷)‘(𝐺‘𝑧))(.r‘𝐷)(𝐺‘𝑧))) |
41 | 25, 28, 35, 29, 40 | syl112anc 1322 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) → (𝐺‘(((invr‘𝐷)‘(𝐺‘𝑧))( ·𝑠
‘𝑊)𝑧)) = (((invr‘𝐷)‘(𝐺‘𝑧))(.r‘𝐷)(𝐺‘𝑧))) |
42 | | lfl1.u |
. . . . . . . 8
⊢ 1 =
(1r‘𝐷) |
43 | 4, 13, 39, 42, 33 | drnginvrl 18589 |
. . . . . . 7
⊢ ((𝐷 ∈ DivRing ∧ (𝐺‘𝑧) ∈ (Base‘𝐷) ∧ (𝐺‘𝑧) ≠ 0 ) →
(((invr‘𝐷)‘(𝐺‘𝑧))(.r‘𝐷)(𝐺‘𝑧)) = 1 ) |
44 | 27, 31, 32, 43 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) →
(((invr‘𝐷)‘(𝐺‘𝑧))(.r‘𝐷)(𝐺‘𝑧)) = 1 ) |
45 | 41, 44 | eqtrd 2644 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) → (𝐺‘(((invr‘𝐷)‘(𝐺‘𝑧))( ·𝑠
‘𝑊)𝑧)) = 1 ) |
46 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 =
(((invr‘𝐷)‘(𝐺‘𝑧))( ·𝑠
‘𝑊)𝑧) → (𝐺‘𝑥) = (𝐺‘(((invr‘𝐷)‘(𝐺‘𝑧))( ·𝑠
‘𝑊)𝑧))) |
47 | 46 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑥 =
(((invr‘𝐷)‘(𝐺‘𝑧))( ·𝑠
‘𝑊)𝑧) → ((𝐺‘𝑥) = 1 ↔ (𝐺‘(((invr‘𝐷)‘(𝐺‘𝑧))( ·𝑠
‘𝑊)𝑧)) = 1 )) |
48 | 47 | rspcev 3282 |
. . . . 5
⊢
(((((invr‘𝐷)‘(𝐺‘𝑧))( ·𝑠
‘𝑊)𝑧) ∈ 𝑉 ∧ (𝐺‘(((invr‘𝐷)‘(𝐺‘𝑧))( ·𝑠
‘𝑊)𝑧)) = 1 ) → ∃𝑥 ∈ 𝑉 (𝐺‘𝑥) = 1 ) |
49 | 38, 45, 48 | syl2anc 691 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) ≠ 0 ) → ∃𝑥 ∈ 𝑉 (𝐺‘𝑥) = 1 ) |
50 | 49 | rexlimdv3a 3015 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → (∃𝑧 ∈ 𝑉 (𝐺‘𝑧) ≠ 0 → ∃𝑥 ∈ 𝑉 (𝐺‘𝑥) = 1 )) |
51 | 50 | 3adant3 1074 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × { 0 })) → (∃𝑧 ∈ 𝑉 (𝐺‘𝑧) ≠ 0 → ∃𝑥 ∈ 𝑉 (𝐺‘𝑥) = 1 )) |
52 | 22, 51 | mpd 15 |
1
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × { 0 })) → ∃𝑥 ∈ 𝑉 (𝐺‘𝑥) = 1 ) |