Metamath Proof Explorer

Theorem zlmodzxzldeplem3

Description: Lemma 3 for zlmodzxzldep . (Contributed by AV, 24-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 ⟩ }
zlmodzxzldeplem.f ⊢ 𝐹 = { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ }
Assertion zlmodzxzldeplem3 ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 )

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 zlmodzxzldeplem.f ⊢ 𝐹 = { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ }
5 ovex ⊢ ( ℤring freeLMod { 0 , 1 } ) ∈ V
6 1 5 eqeltri ⊢ 𝑍 ∈ V
7 1 2 3 4 zlmodzxzldeplem1 ⊢ 𝐹 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } )
8 1 zlmodzxzlmod ⊢ ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) )
9 simpr ⊢ ( ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) ) → ℤring = ( Scalar ‘ 𝑍 ) )
10 9 eqcomd ⊢ ( ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) ) → ( Scalar ‘ 𝑍 ) = ℤring )
11 8 10 ax-mp ⊢ ( Scalar ‘ 𝑍 ) = ℤring
12 11 fveq2i ⊢ ( Base ‘ ( Scalar ‘ 𝑍 ) ) = ( Base ‘ ℤring )
13 zringbas ⊢ ℤ = ( Base ‘ ℤring )
14 13 eqcomi ⊢ ( Base ‘ ℤring ) = ℤ
15 12 14 eqtri ⊢ ( Base ‘ ( Scalar ‘ 𝑍 ) ) = ℤ
16 15 oveq1i ⊢ ( ( Base ‘ ( Scalar ‘ 𝑍 ) ) ↑m { 𝐴 , 𝐵 } ) = ( ℤ ↑m { 𝐴 , 𝐵 } )
17 7 16 eleqtrri ⊢ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑍 ) ) ↑m { 𝐴 , 𝐵 } )
18 3z ⊢ 3 ∈ ℤ
19 6nn ⊢ 6 ∈ ℕ
20 19 nnzi ⊢ 6 ∈ ℤ
21 1 zlmodzxzel ⊢ ( ( 3 ∈ ℤ ∧ 6 ∈ ℤ ) → { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ 𝑍 ) )
22 18 20 21 mp2an ⊢ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ 𝑍 )
23 2z ⊢ 2 ∈ ℤ
24 4z ⊢ 4 ∈ ℤ
25 1 zlmodzxzel ⊢ ( ( 2 ∈ ℤ ∧ 4 ∈ ℤ ) → { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ ( Base ‘ 𝑍 ) )
26 23 24 25 mp2an ⊢ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ ( Base ‘ 𝑍 )
27 2 eleq1i ⊢ ( 𝐴 ∈ ( Base ‘ 𝑍 ) ↔ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ 𝑍 ) )
28 3 eleq1i ⊢ ( 𝐵 ∈ ( Base ‘ 𝑍 ) ↔ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ ( Base ‘ 𝑍 ) )
29 27 28 anbi12i ⊢ ( ( 𝐴 ∈ ( Base ‘ 𝑍 ) ∧ 𝐵 ∈ ( Base ‘ 𝑍 ) ) ↔ ( { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ 𝑍 ) ∧ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ ( Base ‘ 𝑍 ) ) )
30 22 26 29 mpbir2an ⊢ ( 𝐴 ∈ ( Base ‘ 𝑍 ) ∧ 𝐵 ∈ ( Base ‘ 𝑍 ) )
31 prelpwi ⊢ ( ( 𝐴 ∈ ( Base ‘ 𝑍 ) ∧ 𝐵 ∈ ( Base ‘ 𝑍 ) ) → { 𝐴 , 𝐵 } ∈ 𝒫 ( Base ‘ 𝑍 ) )
32 30 31 ax-mp ⊢ { 𝐴 , 𝐵 } ∈ 𝒫 ( Base ‘ 𝑍 )
33 lincval ⊢ ( ( 𝑍 ∈ V ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑍 ) ) ↑m { 𝐴 , 𝐵 } ) ∧ { 𝐴 , 𝐵 } ∈ 𝒫 ( Base ‘ 𝑍 ) ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 𝑍 Σg ( 𝑥 ∈ { 𝐴 , 𝐵 } ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑍 ) 𝑥 ) ) ) )
34 6 17 32 33 mp3an ⊢ ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 𝑍 Σg ( 𝑥 ∈ { 𝐴 , 𝐵 } ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑍 ) 𝑥 ) ) )
35 lmodcmn ⊢ ( 𝑍 ∈ LMod → 𝑍 ∈ CMnd )
36 35 adantr ⊢ ( ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) ) → 𝑍 ∈ CMnd )
37 8 36 ax-mp ⊢ 𝑍 ∈ CMnd
38 prex ⊢ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ V
39 2 38 eqeltri ⊢ 𝐴 ∈ V
40 prex ⊢ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ V
41 3 40 eqeltri ⊢ 𝐵 ∈ V
42 1 2 3 zlmodzxzldeplem ⊢ 𝐴 ≠ 𝐵
43 39 41 42 3pm3.2i ⊢ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 )
44 8 simpli ⊢ 𝑍 ∈ LMod
45 elmapi ⊢ ( 𝐹 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } ) → 𝐹 : { 𝐴 , 𝐵 } ⟶ ℤ )
46 39 prid1 ⊢ 𝐴 ∈ { 𝐴 , 𝐵 }
47 ffvelcdm ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ ℤ ∧ 𝐴 ∈ { 𝐴 , 𝐵 } ) → ( 𝐹 ‘ 𝐴 ) ∈ ℤ )
48 46 47 mpan2 ⊢ ( 𝐹 : { 𝐴 , 𝐵 } ⟶ ℤ → ( 𝐹 ‘ 𝐴 ) ∈ ℤ )
49 7 45 48 mp2b ⊢ ( 𝐹 ‘ 𝐴 ) ∈ ℤ
50 8 9 ax-mp ⊢ ℤring = ( Scalar ‘ 𝑍 )
51 50 eqcomi ⊢ ( Scalar ‘ 𝑍 ) = ℤring
52 51 fveq2i ⊢ ( Base ‘ ( Scalar ‘ 𝑍 ) ) = ( Base ‘ ℤring )
53 52 14 eqtri ⊢ ( Base ‘ ( Scalar ‘ 𝑍 ) ) = ℤ
54 49 53 eleqtrri ⊢ ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑍 ) )
55 2 22 eqeltri ⊢ 𝐴 ∈ ( Base ‘ 𝑍 )
56 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
57 eqid ⊢ ( Scalar ‘ 𝑍 ) = ( Scalar ‘ 𝑍 )
58 eqid ⊢ ( ·𝑠 ‘ 𝑍 ) = ( ·𝑠 ‘ 𝑍 )
59 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑍 ) ) = ( Base ‘ ( Scalar ‘ 𝑍 ) )
60 56 57 58 59 lmodvscl ⊢ ( ( 𝑍 ∈ LMod ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑍 ) ) ∧ 𝐴 ∈ ( Base ‘ 𝑍 ) ) → ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ∈ ( Base ‘ 𝑍 ) )
61 44 54 55 60 mp3an ⊢ ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ∈ ( Base ‘ 𝑍 )
62 41 prid2 ⊢ 𝐵 ∈ { 𝐴 , 𝐵 }
63 ffvelcdm ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ ℤ ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) → ( 𝐹 ‘ 𝐵 ) ∈ ℤ )
64 62 63 mpan2 ⊢ ( 𝐹 : { 𝐴 , 𝐵 } ⟶ ℤ → ( 𝐹 ‘ 𝐵 ) ∈ ℤ )
65 7 45 64 mp2b ⊢ ( 𝐹 ‘ 𝐵 ) ∈ ℤ
66 65 53 eleqtrri ⊢ ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ( Scalar ‘ 𝑍 ) )
67 3 26 eqeltri ⊢ 𝐵 ∈ ( Base ‘ 𝑍 )
68 56 57 58 59 lmodvscl ⊢ ( ( 𝑍 ∈ LMod ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ ( Scalar ‘ 𝑍 ) ) ∧ 𝐵 ∈ ( Base ‘ 𝑍 ) ) → ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ∈ ( Base ‘ 𝑍 ) )
69 44 66 67 68 mp3an ⊢ ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ∈ ( Base ‘ 𝑍 )
70 61 69 pm3.2i ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ∈ ( Base ‘ 𝑍 ) ∧ ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ∈ ( Base ‘ 𝑍 ) )
71 eqid ⊢ ( +g ‘ 𝑍 ) = ( +g ‘ 𝑍 )
72 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
73 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
74 72 73 oveq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑍 ) 𝑥 ) = ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) )
75 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
76 id ⊢ ( 𝑥 = 𝐵 → 𝑥 = 𝐵 )
77 75 76 oveq12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑍 ) 𝑥 ) = ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) )
78 56 71 74 77 gsumpr ⊢ ( ( 𝑍 ∈ CMnd ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ∈ ( Base ‘ 𝑍 ) ∧ ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑍 Σg ( 𝑥 ∈ { 𝐴 , 𝐵 } ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑍 ) 𝑥 ) ) ) = ( ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ( +g ‘ 𝑍 ) ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ) )
79 37 43 70 78 mp3an ⊢ ( 𝑍 Σg ( 𝑥 ∈ { 𝐴 , 𝐵 } ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑍 ) 𝑥 ) ) ) = ( ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ( +g ‘ 𝑍 ) ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) )
80 4 fveq1i ⊢ ( 𝐹 ‘ 𝐴 ) = ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝐴 )
81 2ex ⊢ 2 ∈ V
82 39 81 fvpr1 ⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝐴 ) = 2 )
83 42 82 ax-mp ⊢ ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝐴 ) = 2
84 80 83 eqtri ⊢ ( 𝐹 ‘ 𝐴 ) = 2
85 84 oveq1i ⊢ ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) = ( 2 ( ·𝑠 ‘ 𝑍 ) 𝐴 )
86 4 fveq1i ⊢ ( 𝐹 ‘ 𝐵 ) = ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝐵 )
87 negex ⊢ - 3 ∈ V
88 41 87 fvpr2 ⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝐵 ) = - 3 )
89 42 88 ax-mp ⊢ ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝐵 ) = - 3
90 86 89 eqtri ⊢ ( 𝐹 ‘ 𝐵 ) = - 3
91 90 oveq1i ⊢ ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) = ( - 3 ( ·𝑠 ‘ 𝑍 ) 𝐵 )
92 85 91 oveq12i ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ( +g ‘ 𝑍 ) ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ) = ( ( 2 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ( +g ‘ 𝑍 ) ( - 3 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) )
93 eqid ⊢ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
94 1 93 zlmodzxz0 ⊢ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = ( 0g ‘ 𝑍 )
95 94 eqcomi ⊢ ( 0g ‘ 𝑍 ) = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
96 1 2 3 95 71 58 zlmodzxzequap ⊢ ( ( 2 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ( +g ‘ 𝑍 ) ( - 3 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ) = ( 0g ‘ 𝑍 )
97 92 96 eqtri ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ( +g ‘ 𝑍 ) ( ( 𝐹 ‘ 𝐵 ) ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ) = ( 0g ‘ 𝑍 )
98 34 79 97 3eqtri ⊢ ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 )