Metamath Proof Explorer

Theorem m2detleiblem4

Description: Lemma 4 for m2detleib . (Contributed by AV, 20-Dec-2018) (Proof shortened by AV, 2-Jan-2019)

Ref Expression
Hypotheses m2detleiblem2.n ⊢ 𝑁 = { 1 , 2 }
m2detleiblem2.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
m2detleiblem2.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
m2detleiblem2.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
m2detleiblem2.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
m2detleiblem3.m ⊢ · = ( +g ‘ 𝐺 )
Assertion m2detleiblem4 ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) )

Proof

Step Hyp Ref Expression
1 m2detleiblem2.n ⊢ 𝑁 = { 1 , 2 }
2 m2detleiblem2.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
3 m2detleiblem2.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4 m2detleiblem2.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
5 m2detleiblem2.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
6 m2detleiblem3.m ⊢ · = ( +g ‘ 𝐺 )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 5 7 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐺 )
9 5 fvexi ⊢ 𝐺 ∈ V
10 9 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → 𝐺 ∈ V )
11 1ex ⊢ 1 ∈ V
12 2nn ⊢ 2 ∈ ℕ
13 prex ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ V
14 13 prid2 ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
15 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
16 15 2 1 symg2bas ⊢ ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → 𝑃 = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
17 14 16 eleqtrrid ⊢ ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃 )
18 11 12 17 mp2an ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃
19 eleq1 ⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑄 ∈ 𝑃 ↔ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃 ) )
20 18 19 mpbiri ⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → 𝑄 ∈ 𝑃 )
21 1 oveq1i ⊢ ( 𝑁 Mat 𝑅 ) = ( { 1 , 2 } Mat 𝑅 )
22 3 21 eqtri ⊢ 𝐴 = ( { 1 , 2 } Mat 𝑅 )
23 1 fveq2i ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ { 1 , 2 } )
24 23 fveq2i ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ { 1 , 2 } ) )
25 2 24 eqtri ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ { 1 , 2 } ) )
26 22 4 25 matepmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ { 1 , 2 } ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
27 20 26 syl3an2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ { 1 , 2 } ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
28 1 mpteq1i ⊢ ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) = ( 𝑛 ∈ { 1 , 2 } ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) )
29 28 fmpt ⊢ ( ∀ 𝑛 ∈ { 1 , 2 } ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) ↔ ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) : { 1 , 2 } ⟶ ( Base ‘ 𝑅 ) )
30 27 29 sylib ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) : { 1 , 2 } ⟶ ( Base ‘ 𝑅 ) )
31 8 6 10 30 gsumpr12val ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 1 ) · ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 2 ) ) )
32 11 prid1 ⊢ 1 ∈ { 1 , 2 }
33 32 1 eleqtrri ⊢ 1 ∈ 𝑁
34 3 4 2 matepmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ 𝑁 ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
35 20 34 syl3an2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ 𝑁 ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
36 fveq2 ⊢ ( 𝑛 = 1 → ( 𝑄 ‘ 𝑛 ) = ( 𝑄 ‘ 1 ) )
37 id ⊢ ( 𝑛 = 1 → 𝑛 = 1 )
38 36 37 oveq12d ⊢ ( 𝑛 = 1 → ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) = ( ( 𝑄 ‘ 1 ) 𝑀 1 ) )
39 38 eleq1d ⊢ ( 𝑛 = 1 → ( ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) ↔ ( ( 𝑄 ‘ 1 ) 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) ) )
40 39 rspcva ⊢ ( ( 1 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑄 ‘ 1 ) 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) )
41 33 35 40 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑄 ‘ 1 ) 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) )
42 eqid ⊢ ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) = ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) )
43 38 42 fvmptg ⊢ ( ( 1 ∈ 𝑁 ∧ ( ( 𝑄 ‘ 1 ) 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 1 ) = ( ( 𝑄 ‘ 1 ) 𝑀 1 ) )
44 33 41 43 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 1 ) = ( ( 𝑄 ‘ 1 ) 𝑀 1 ) )
45 fveq1 ⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑄 ‘ 1 ) = ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) )
46 1ne2 ⊢ 1 ≠ 2
47 2ex ⊢ 2 ∈ V
48 11 47 fvpr1 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) = 2 )
49 46 48 ax-mp ⊢ ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) = 2
50 45 49 eqtrdi ⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑄 ‘ 1 ) = 2 )
51 50 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( 𝑄 ‘ 1 ) = 2 )
52 51 oveq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑄 ‘ 1 ) 𝑀 1 ) = ( 2 𝑀 1 ) )
53 44 52 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 1 ) = ( 2 𝑀 1 ) )
54 47 prid2 ⊢ 2 ∈ { 1 , 2 }
55 54 1 eleqtrri ⊢ 2 ∈ 𝑁
56 fveq2 ⊢ ( 𝑛 = 2 → ( 𝑄 ‘ 𝑛 ) = ( 𝑄 ‘ 2 ) )
57 id ⊢ ( 𝑛 = 2 → 𝑛 = 2 )
58 56 57 oveq12d ⊢ ( 𝑛 = 2 → ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) = ( ( 𝑄 ‘ 2 ) 𝑀 2 ) )
59 58 eleq1d ⊢ ( 𝑛 = 2 → ( ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) ↔ ( ( 𝑄 ‘ 2 ) 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) ) )
60 59 rspcva ⊢ ( ( 2 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑄 ‘ 2 ) 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) )
61 55 35 60 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑄 ‘ 2 ) 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) )
62 58 42 fvmptg ⊢ ( ( 2 ∈ 𝑁 ∧ ( ( 𝑄 ‘ 2 ) 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 2 ) = ( ( 𝑄 ‘ 2 ) 𝑀 2 ) )
63 55 61 62 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 2 ) = ( ( 𝑄 ‘ 2 ) 𝑀 2 ) )
64 fveq1 ⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑄 ‘ 2 ) = ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) )
65 47 11 fvpr2 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) = 1 )
66 46 65 ax-mp ⊢ ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) = 1
67 64 66 eqtrdi ⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑄 ‘ 2 ) = 1 )
68 67 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( 𝑄 ‘ 2 ) = 1 )
69 68 oveq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑄 ‘ 2 ) 𝑀 2 ) = ( 1 𝑀 2 ) )
70 63 69 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 2 ) = ( 1 𝑀 2 ) )
71 53 70 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 1 ) · ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 2 ) ) = ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) )
72 31 71 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) )