Metamath Proof Explorer


Theorem ldepsnlinclem2

Description: Lemma 2 for ldepsnlinc . (Contributed by AV, 25-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxzldep.z 𝑍 = ( ℤring freeLMod { 0 , 1 } )
zlmodzxzldep.a 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
zlmodzxzldep.b 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
Assertion ldepsnlinclem2 ( 𝐹 ∈ ( ( Base ‘ ℤring ) ↑m { 𝐴 } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) ≠ 𝐵 )

Proof

Step Hyp Ref Expression
1 zlmodzxzldep.z 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2 zlmodzxzldep.a 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
3 zlmodzxzldep.b 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
4 elmapi ( 𝐹 ∈ ( ( Base ‘ ℤring ) ↑m { 𝐴 } ) → 𝐹 : { 𝐴 } ⟶ ( Base ‘ ℤring ) )
5 prex { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ V
6 2 5 eqeltri 𝐴 ∈ V
7 6 fsn2 ( 𝐹 : { 𝐴 } ⟶ ( Base ‘ ℤring ) ↔ ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) )
8 oveq1 ( 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ( linC ‘ 𝑍 ) { 𝐴 } ) )
9 8 adantl ( ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ( linC ‘ 𝑍 ) { 𝐴 } ) )
10 1 zlmodzxzlmod ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) )
11 10 simpli 𝑍 ∈ LMod
12 11 a1i ( ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) → 𝑍 ∈ LMod )
13 3z 3 ∈ ℤ
14 6nn 6 ∈ ℕ
15 14 nnzi 6 ∈ ℤ
16 1 zlmodzxzel ( ( 3 ∈ ℤ ∧ 6 ∈ ℤ ) → { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ 𝑍 ) )
17 13 15 16 mp2an { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ 𝑍 )
18 2 17 eqeltri 𝐴 ∈ ( Base ‘ 𝑍 )
19 18 a1i ( ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) → 𝐴 ∈ ( Base ‘ 𝑍 ) )
20 simpl ( ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) → ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) )
21 eqid ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
22 10 simpri ring = ( Scalar ‘ 𝑍 )
23 eqid ( Base ‘ ℤring ) = ( Base ‘ ℤring )
24 eqid ( ·𝑠𝑍 ) = ( ·𝑠𝑍 )
25 21 22 23 24 lincvalsng ( ( 𝑍 ∈ LMod ∧ 𝐴 ∈ ( Base ‘ 𝑍 ) ∧ ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ) → ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ( linC ‘ 𝑍 ) { 𝐴 } ) = ( ( 𝐹𝐴 ) ( ·𝑠𝑍 ) 𝐴 ) )
26 12 19 20 25 syl3anc ( ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) → ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ( linC ‘ 𝑍 ) { 𝐴 } ) = ( ( 𝐹𝐴 ) ( ·𝑠𝑍 ) 𝐴 ) )
27 9 26 eqtrd ( ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) = ( ( 𝐹𝐴 ) ( ·𝑠𝑍 ) 𝐴 ) )
28 eqid { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
29 eqid ( -g𝑍 ) = ( -g𝑍 )
30 1 28 24 29 2 3 zlmodzxznm 𝑖 ∈ ℤ ( ( 𝑖 ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ( ·𝑠𝑍 ) 𝐵 ) ≠ 𝐴 )
31 r19.26 ( ∀ 𝑖 ∈ ℤ ( ( 𝑖 ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ( ·𝑠𝑍 ) 𝐵 ) ≠ 𝐴 ) ↔ ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠𝑍 ) 𝐵 ) ≠ 𝐴 ) )
32 oveq1 ( 𝑖 = ( 𝐹𝐴 ) → ( 𝑖 ( ·𝑠𝑍 ) 𝐴 ) = ( ( 𝐹𝐴 ) ( ·𝑠𝑍 ) 𝐴 ) )
33 32 neeq1d ( 𝑖 = ( 𝐹𝐴 ) → ( ( 𝑖 ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 ↔ ( ( 𝐹𝐴 ) ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 ) )
34 33 rspcv ( ( 𝐹𝐴 ) ∈ ℤ → ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 → ( ( 𝐹𝐴 ) ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 ) )
35 zringbas ℤ = ( Base ‘ ℤring )
36 35 eqcomi ( Base ‘ ℤring ) = ℤ
37 36 eleq2i ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ↔ ( 𝐹𝐴 ) ∈ ℤ )
38 37 biimpi ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) → ( 𝐹𝐴 ) ∈ ℤ )
39 38 adantr ( ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) → ( 𝐹𝐴 ) ∈ ℤ )
40 34 39 syl11 ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 → ( ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) → ( ( 𝐹𝐴 ) ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 ) )
41 40 adantr ( ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠𝑍 ) 𝐵 ) ≠ 𝐴 ) → ( ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) → ( ( 𝐹𝐴 ) ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 ) )
42 31 41 sylbi ( ∀ 𝑖 ∈ ℤ ( ( 𝑖 ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ( ·𝑠𝑍 ) 𝐵 ) ≠ 𝐴 ) → ( ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) → ( ( 𝐹𝐴 ) ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 ) )
43 30 42 ax-mp ( ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) → ( ( 𝐹𝐴 ) ( ·𝑠𝑍 ) 𝐴 ) ≠ 𝐵 )
44 27 43 eqnetrd ( ( ( 𝐹𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) ≠ 𝐵 )
45 7 44 sylbi ( 𝐹 : { 𝐴 } ⟶ ( Base ‘ ℤring ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) ≠ 𝐵 )
46 4 45 syl ( 𝐹 ∈ ( ( Base ‘ ℤring ) ↑m { 𝐴 } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) ≠ 𝐵 )