Metamath Proof Explorer

Theorem ldepsnlinclem1

Description: Lemma 1 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 ldepsnlinclem1 ( 𝐹 ∈ ( ( 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 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ V
6 3 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 2z ⊢ 2 ∈ ℤ
14 4z ⊢ 4 ∈ ℤ
15 1 zlmodzxzel ⊢ ( ( 2 ∈ ℤ ∧ 4 ∈ ℤ ) → { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ ( Base ‘ 𝑍 ) )
16 13 14 15 mp2an ⊢ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ ( Base ‘ 𝑍 )
17 3 16 eqeltri ⊢ 𝐵 ∈ ( Base ‘ 𝑍 )
18 17 a1i ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) → 𝐵 ∈ ( Base ‘ 𝑍 ) )
19 simpl ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) → ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) )
20 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
21 10 simpri ⊢ ℤring = ( Scalar ‘ 𝑍 )
22 eqid ⊢ ( Base ‘ ℤring ) = ( Base ‘ ℤring )
23 eqid ⊢ ( ·𝑠 ‘ 𝑍 ) = ( ·𝑠 ‘ 𝑍 )
24 20 21 22 23 lincvalsng ⊢ ( ( 𝑍 ∈ LMod ∧ 𝐵 ∈ ( Base ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) ) → ( { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ( linC ‘ 𝑍 ) { 𝐵 } ) = ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) )
25 12 18 19 24 syl3anc ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) → ( { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ( linC ‘ 𝑍 ) { 𝐵 } ) = ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) )
26 9 25 eqtrd ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐵 } ) = ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) )
27 eqid ⊢ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
28 eqid ⊢ ( -g ‘ 𝑍 ) = ( -g ‘ 𝑍 )
29 1 27 23 28 2 3 zlmodzxznm ⊢ ∀ 𝑖 ∈ ℤ ( ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 )
30 r19.26 ⊢ ( ∀ 𝑖 ∈ ℤ ( ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) ↔ ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) )
31 oveq1 ⊢ ( 𝑖 = ( 𝐹 ‘ 𝐵 ) → ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) = ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) )
32 31 neeq1d ⊢ ( 𝑖 = ( 𝐹 ‘ 𝐵 ) → ( ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ↔ ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) )
33 32 rspcv ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ℤ → ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 → ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) )
34 zringbas ⊢ ℤ = ( Base ‘ ℤring )
35 34 eqcomi ⊢ ( Base ‘ ℤring ) = ℤ
36 35 eleq2i ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) ↔ ( 𝐹 ‘ 𝐵 ) ∈ ℤ )
37 36 biimpi ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) → ( 𝐹 ‘ 𝐵 ) ∈ ℤ )
38 37 adantr ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) → ( 𝐹 ‘ 𝐵 ) ∈ ℤ )
39 33 38 syl11 ⊢ ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 → ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) → ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) )
40 39 adantl ⊢ ( ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) → ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) → ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) )
41 30 40 sylbi ⊢ ( ∀ 𝑖 ∈ ℤ ( ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) → ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) → ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) )
42 29 41 ax-mp ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) → ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 )
43 26 42 eqnetrd ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐵 } ) ≠ 𝐴 )
44 7 43 sylbi ⊢ ( 𝐹 : { 𝐵 } ⟶ ( Base ‘ ℤring ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐵 } ) ≠ 𝐴 )
45 4 44 syl ⊢ ( 𝐹 ∈ ( ( Base ‘ ℤring ) ↑m { 𝐵 } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐵 } ) ≠ 𝐴 )