Metamath Proof Explorer

Theorem zlmlem

Description: Lemma for zlmbas and zlmplusg . (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 3-Nov-2024)

Ref Expression
Hypotheses zlmbas.w ⊢ W = ℤMod ⁡ G
zlmlem.2 ⊢ E = Slot E ⁡ ndx
zlmlem.3 ⊢ E ⁡ ndx ≠ Scalar ⁡ ndx
zlmlem.4 ⊢ E ⁡ ndx ≠ ⋅ ndx
Assertion zlmlem ⊢ E ⁡ G = E ⁡ W

Proof

Step Hyp Ref Expression
1 zlmbas.w ⊢ W = ℤMod ⁡ G
2 zlmlem.2 ⊢ E = Slot E ⁡ ndx
3 zlmlem.3 ⊢ E ⁡ ndx ≠ Scalar ⁡ ndx
4 zlmlem.4 ⊢ E ⁡ ndx ≠ ⋅ ndx
5 2 3 setsnid ⊢ E ⁡ G = E ⁡ G sSet Scalar ⁡ ndx ℤ ring
6 2 4 setsnid ⊢ E ⁡ G sSet Scalar ⁡ ndx ℤ ring = E ⁡ G sSet Scalar ⁡ ndx ℤ ring sSet ⋅ ndx ⋅ G
7 5 6 eqtri ⊢ E ⁡ G = E ⁡ G sSet Scalar ⁡ ndx ℤ ring sSet ⋅ ndx ⋅ G
8 eqid ⊢ ⋅ G = ⋅ G
9 1 8 zlmval ⊢ G ∈ V → W = G sSet Scalar ⁡ ndx ℤ ring sSet ⋅ ndx ⋅ G
10 9 fveq2d ⊢ G ∈ V → E ⁡ W = E ⁡ G sSet Scalar ⁡ ndx ℤ ring sSet ⋅ ndx ⋅ G
11 7 10 eqtr4id ⊢ G ∈ V → E ⁡ G = E ⁡ W
12 2 str0 ⊢ ∅ = E ⁡ ∅
13 12 eqcomi ⊢ E ⁡ ∅ = ∅
14 13 1 fveqprc ⊢ ¬ G ∈ V → E ⁡ G = E ⁡ W
15 11 14 pm2.61i ⊢ E ⁡ G = E ⁡ W