Step |
Hyp |
Ref |
Expression |
1 |
|
lfl1.d |
⊢ 𝐷 = ( Scalar ‘ 𝑊 ) |
2 |
|
lfl1.o |
⊢ 0 = ( 0g ‘ 𝐷 ) |
3 |
|
lfl1.u |
⊢ 1 = ( 1r ‘ 𝐷 ) |
4 |
|
lfl1.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
5 |
|
lfl1.f |
⊢ 𝐹 = ( LFnl ‘ 𝑊 ) |
6 |
|
nne |
⊢ ( ¬ ( 𝐺 ‘ 𝑧 ) ≠ 0 ↔ ( 𝐺 ‘ 𝑧 ) = 0 ) |
7 |
6
|
ralbii |
⊢ ( ∀ 𝑧 ∈ 𝑉 ¬ ( 𝐺 ‘ 𝑧 ) ≠ 0 ↔ ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) = 0 ) |
8 |
|
eqid |
⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) |
9 |
1 8 4 5
|
lflf |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝐷 ) ) |
10 |
9
|
ffnd |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → 𝐺 Fn 𝑉 ) |
11 |
|
fconstfv |
⊢ ( 𝐺 : 𝑉 ⟶ { 0 } ↔ ( 𝐺 Fn 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) = 0 ) ) |
12 |
11
|
simplbi2 |
⊢ ( 𝐺 Fn 𝑉 → ( ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) = 0 → 𝐺 : 𝑉 ⟶ { 0 } ) ) |
13 |
10 12
|
syl |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) = 0 → 𝐺 : 𝑉 ⟶ { 0 } ) ) |
14 |
2
|
fvexi |
⊢ 0 ∈ V |
15 |
14
|
fconst2 |
⊢ ( 𝐺 : 𝑉 ⟶ { 0 } ↔ 𝐺 = ( 𝑉 × { 0 } ) ) |
16 |
13 15
|
syl6ib |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) = 0 → 𝐺 = ( 𝑉 × { 0 } ) ) ) |
17 |
7 16
|
syl5bi |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( ∀ 𝑧 ∈ 𝑉 ¬ ( 𝐺 ‘ 𝑧 ) ≠ 0 → 𝐺 = ( 𝑉 × { 0 } ) ) ) |
18 |
17
|
necon3ad |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ≠ ( 𝑉 × { 0 } ) → ¬ ∀ 𝑧 ∈ 𝑉 ¬ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) ) |
19 |
|
dfrex2 |
⊢ ( ∃ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) ≠ 0 ↔ ¬ ∀ 𝑧 ∈ 𝑉 ¬ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) |
20 |
18 19
|
syl6ibr |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ≠ ( 𝑉 × { 0 } ) → ∃ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) ≠ 0 ) ) |
21 |
20
|
3impia |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ∃ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) ≠ 0 ) |
22 |
|
simp1l |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑊 ∈ LVec ) |
23 |
|
lveclmod |
⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod ) |
24 |
22 23
|
syl |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑊 ∈ LMod ) |
25 |
1
|
lvecdrng |
⊢ ( 𝑊 ∈ LVec → 𝐷 ∈ DivRing ) |
26 |
22 25
|
syl |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝐷 ∈ DivRing ) |
27 |
|
simp1r |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝐺 ∈ 𝐹 ) |
28 |
|
simp2 |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑧 ∈ 𝑉 ) |
29 |
1 8 4 5
|
lflcl |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) ) |
30 |
22 27 28 29
|
syl3anc |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) ) |
31 |
|
simp3 |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 ) |
32 |
|
eqid |
⊢ ( invr ‘ 𝐷 ) = ( invr ‘ 𝐷 ) |
33 |
8 2 32
|
drnginvrcl |
⊢ ( ( 𝐷 ∈ DivRing ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝐷 ) ) |
34 |
26 30 31 33
|
syl3anc |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝐷 ) ) |
35 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) |
36 |
4 1 35 8
|
lmodvscl |
⊢ ( ( 𝑊 ∈ LMod ∧ ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ 𝑉 ) → ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 ) |
37 |
24 34 28 36
|
syl3anc |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 ) |
38 |
|
eqid |
⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 ) |
39 |
1 8 38 4 35 5
|
lflmul |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑧 ) ) ) |
40 |
24 27 34 28 39
|
syl112anc |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑧 ) ) ) |
41 |
8 2 38 3 32
|
drnginvrl |
⊢ ( ( 𝐷 ∈ DivRing ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑧 ) ) = 1 ) |
42 |
26 30 31 41
|
syl3anc |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑧 ) ) = 1 ) |
43 |
40 42
|
eqtrd |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = 1 ) |
44 |
|
fveqeq2 |
⊢ ( 𝑥 = ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) → ( ( 𝐺 ‘ 𝑥 ) = 1 ↔ ( 𝐺 ‘ ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = 1 ) ) |
45 |
44
|
rspcev |
⊢ ( ( ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 ∧ ( 𝐺 ‘ ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = 1 ) → ∃ 𝑥 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) = 1 ) |
46 |
37 43 45
|
syl2anc |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ∃ 𝑥 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) = 1 ) |
47 |
46
|
rexlimdv3a |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( ∃ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) ≠ 0 → ∃ 𝑥 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) = 1 ) ) |
48 |
47
|
3adant3 |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( ∃ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) ≠ 0 → ∃ 𝑥 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) = 1 ) ) |
49 |
21 48
|
mpd |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ∃ 𝑥 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) = 1 ) |