Step |
Hyp |
Ref |
Expression |
1 |
|
lindfind2.k |
⊢ 𝐾 = ( LSpan ‘ 𝑊 ) |
2 |
|
lindfind2.l |
⊢ 𝐿 = ( Scalar ‘ 𝑊 ) |
3 |
|
simp1l |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → 𝑊 ∈ LMod ) |
4 |
|
simp2 |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → 𝐹 LIndF 𝑊 ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) |
6 |
5
|
lindff |
⊢ ( ( 𝐹 LIndF 𝑊 ∧ 𝑊 ∈ LMod ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) ) |
7 |
4 3 6
|
syl2anc |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) ) |
8 |
|
simp3 |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → 𝐸 ∈ dom 𝐹 ) |
9 |
7 8
|
ffvelrnd |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐸 ) ∈ ( Base ‘ 𝑊 ) ) |
10 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) |
11 |
|
eqid |
⊢ ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐿 ) |
12 |
5 2 10 11
|
lmodvs1 |
⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐹 ‘ 𝐸 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 1r ‘ 𝐿 ) ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝐸 ) ) = ( 𝐹 ‘ 𝐸 ) ) |
13 |
3 9 12
|
syl2anc |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ( ( 1r ‘ 𝐿 ) ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝐸 ) ) = ( 𝐹 ‘ 𝐸 ) ) |
14 |
|
nzrring |
⊢ ( 𝐿 ∈ NzRing → 𝐿 ∈ Ring ) |
15 |
|
eqid |
⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 ) |
16 |
15 11
|
ringidcl |
⊢ ( 𝐿 ∈ Ring → ( 1r ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) ) |
17 |
14 16
|
syl |
⊢ ( 𝐿 ∈ NzRing → ( 1r ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) ) |
18 |
17
|
adantl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) → ( 1r ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) ) |
19 |
18
|
3ad2ant1 |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ( 1r ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) ) |
20 |
|
eqid |
⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 ) |
21 |
11 20
|
nzrnz |
⊢ ( 𝐿 ∈ NzRing → ( 1r ‘ 𝐿 ) ≠ ( 0g ‘ 𝐿 ) ) |
22 |
21
|
adantl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) → ( 1r ‘ 𝐿 ) ≠ ( 0g ‘ 𝐿 ) ) |
23 |
22
|
3ad2ant1 |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ( 1r ‘ 𝐿 ) ≠ ( 0g ‘ 𝐿 ) ) |
24 |
10 1 2 20 15
|
lindfind |
⊢ ( ( ( 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) ∧ ( ( 1r ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 1r ‘ 𝐿 ) ≠ ( 0g ‘ 𝐿 ) ) ) → ¬ ( ( 1r ‘ 𝐿 ) ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝐸 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝐸 } ) ) ) ) |
25 |
4 8 19 23 24
|
syl22anc |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ¬ ( ( 1r ‘ 𝐿 ) ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝐸 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝐸 } ) ) ) ) |
26 |
13 25
|
eqneltrrd |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ¬ ( 𝐹 ‘ 𝐸 ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝐸 } ) ) ) ) |