Step |
Hyp |
Ref |
Expression |
1 |
|
lkr0f.d |
⊢ 𝐷 = ( Scalar ‘ 𝑊 ) |
2 |
|
lkr0f.o |
⊢ 0 = ( 0g ‘ 𝐷 ) |
3 |
|
lkr0f.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
4 |
|
lkr0f.f |
⊢ 𝐹 = ( LFnl ‘ 𝑊 ) |
5 |
|
lkr0f.k |
⊢ 𝐾 = ( LKer ‘ 𝑊 ) |
6 |
|
eqid |
⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) |
7 |
1 6 3 4
|
lflf |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝐷 ) ) |
8 |
7
|
ffnd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 Fn 𝑉 ) |
9 |
8
|
adantr |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) → 𝐺 Fn 𝑉 ) |
10 |
1 2 4 5
|
lkrval |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = ( ◡ 𝐺 “ { 0 } ) ) |
11 |
10
|
eqeq1d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) ) |
12 |
11
|
biimpa |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) → ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) |
13 |
2
|
fvexi |
⊢ 0 ∈ V |
14 |
13
|
fconst2 |
⊢ ( 𝐺 : 𝑉 ⟶ { 0 } ↔ 𝐺 = ( 𝑉 × { 0 } ) ) |
15 |
|
fconst4 |
⊢ ( 𝐺 : 𝑉 ⟶ { 0 } ↔ ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) ) |
16 |
14 15
|
bitr3i |
⊢ ( 𝐺 = ( 𝑉 × { 0 } ) ↔ ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) ) |
17 |
9 12 16
|
sylanbrc |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) → 𝐺 = ( 𝑉 × { 0 } ) ) |
18 |
17
|
ex |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 → 𝐺 = ( 𝑉 × { 0 } ) ) ) |
19 |
16
|
biimpi |
⊢ ( 𝐺 = ( 𝑉 × { 0 } ) → ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) ) |
20 |
19
|
adantl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) ) |
21 |
|
simpr |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → 𝐺 = ( 𝑉 × { 0 } ) ) |
22 |
|
eqid |
⊢ ( LFnl ‘ 𝑊 ) = ( LFnl ‘ 𝑊 ) |
23 |
1 2 3 22
|
lfl0f |
⊢ ( 𝑊 ∈ LMod → ( 𝑉 × { 0 } ) ∈ ( LFnl ‘ 𝑊 ) ) |
24 |
23
|
adantr |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝑉 × { 0 } ) ∈ ( LFnl ‘ 𝑊 ) ) |
25 |
21 24
|
eqeltrd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → 𝐺 ∈ ( LFnl ‘ 𝑊 ) ) |
26 |
1 2 22 5
|
lkrval |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ ( LFnl ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐺 ) = ( ◡ 𝐺 “ { 0 } ) ) |
27 |
25 26
|
syldan |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) = ( ◡ 𝐺 “ { 0 } ) ) |
28 |
27
|
eqeq1d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) ) |
29 |
|
ffn |
⊢ ( 𝐺 : 𝑉 ⟶ { 0 } → 𝐺 Fn 𝑉 ) |
30 |
14 29
|
sylbir |
⊢ ( 𝐺 = ( 𝑉 × { 0 } ) → 𝐺 Fn 𝑉 ) |
31 |
30
|
adantl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → 𝐺 Fn 𝑉 ) |
32 |
31
|
biantrurd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( ( ◡ 𝐺 “ { 0 } ) = 𝑉 ↔ ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) ) ) |
33 |
28 32
|
bitrd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) ) ) |
34 |
20 33
|
mpbird |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) = 𝑉 ) |
35 |
34
|
ex |
⊢ ( 𝑊 ∈ LMod → ( 𝐺 = ( 𝑉 × { 0 } ) → ( 𝐾 ‘ 𝐺 ) = 𝑉 ) ) |
36 |
35
|
adantr |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 = ( 𝑉 × { 0 } ) → ( 𝐾 ‘ 𝐺 ) = 𝑉 ) ) |
37 |
18 36
|
impbid |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { 0 } ) ) ) |