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 N = 1 2
m2detleiblem2.p P = Base SymGrp N
m2detleiblem2.a A = N Mat R
m2detleiblem2.b B = Base A
m2detleiblem2.g G = mulGrp R
m2detleiblem3.m · ˙ = + G
Assertion m2detleiblem4 R Ring Q = 1 2 2 1 M B G n N Q n M n = 2 M 1 · ˙ 1 M 2

Proof

Step Hyp Ref Expression
1 m2detleiblem2.n N = 1 2
2 m2detleiblem2.p P = Base SymGrp N
3 m2detleiblem2.a A = N Mat R
4 m2detleiblem2.b B = Base A
5 m2detleiblem2.g G = mulGrp R
6 m2detleiblem3.m · ˙ = + G
7 eqid Base R = Base R
8 5 7 mgpbas Base R = Base G
9 5 fvexi G V
10 9 a1i R Ring Q = 1 2 2 1 M B G 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 N = SymGrp N
16 15 2 1 symg2bas 1 V 2 P = 1 1 2 2 1 2 2 1
17 14 16 eleqtrrid 1 V 2 1 2 2 1 P
18 11 12 17 mp2an 1 2 2 1 P
19 eleq1 Q = 1 2 2 1 Q P 1 2 2 1 P
20 18 19 mpbiri Q = 1 2 2 1 Q P
21 1 oveq1i N Mat R = 1 2 Mat R
22 3 21 eqtri A = 1 2 Mat R
23 1 fveq2i SymGrp N = SymGrp 1 2
24 23 fveq2i Base SymGrp N = Base SymGrp 1 2
25 2 24 eqtri P = Base SymGrp 1 2
26 22 4 25 matepmcl R Ring Q P M B n 1 2 Q n M n Base R
27 20 26 syl3an2 R Ring Q = 1 2 2 1 M B n 1 2 Q n M n Base R
28 1 mpteq1i n N Q n M n = n 1 2 Q n M n
29 28 fmpt n 1 2 Q n M n Base R n N Q n M n : 1 2 Base R
30 27 29 sylib R Ring Q = 1 2 2 1 M B n N Q n M n : 1 2 Base R
31 8 6 10 30 gsumpr12val R Ring Q = 1 2 2 1 M B G n N Q n M n = n N Q n M n 1 · ˙ n N Q n M n 2
32 11 prid1 1 1 2
33 32 1 eleqtrri 1 N
34 3 4 2 matepmcl R Ring Q P M B n N Q n M n Base R
35 20 34 syl3an2 R Ring Q = 1 2 2 1 M B n N Q n M n Base R
36 fveq2 n = 1 Q n = Q 1
37 id n = 1 n = 1
38 36 37 oveq12d n = 1 Q n M n = Q 1 M 1
39 38 eleq1d n = 1 Q n M n Base R Q 1 M 1 Base R
40 39 rspcva 1 N n N Q n M n Base R Q 1 M 1 Base R
41 33 35 40 sylancr R Ring Q = 1 2 2 1 M B Q 1 M 1 Base R
42 eqid n N Q n M n = n N Q n M n
43 38 42 fvmptg 1 N Q 1 M 1 Base R n N Q n M n 1 = Q 1 M 1
44 33 41 43 sylancr R Ring Q = 1 2 2 1 M B n N Q n M n 1 = Q 1 M 1
45 fveq1 Q = 1 2 2 1 Q 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 Q = 1 2 2 1 Q 1 = 2
51 50 3ad2ant2 R Ring Q = 1 2 2 1 M B Q 1 = 2
52 51 oveq1d R Ring Q = 1 2 2 1 M B Q 1 M 1 = 2 M 1
53 44 52 eqtrd R Ring Q = 1 2 2 1 M B n N Q n M n 1 = 2 M 1
54 47 prid2 2 1 2
55 54 1 eleqtrri 2 N
56 fveq2 n = 2 Q n = Q 2
57 id n = 2 n = 2
58 56 57 oveq12d n = 2 Q n M n = Q 2 M 2
59 58 eleq1d n = 2 Q n M n Base R Q 2 M 2 Base R
60 59 rspcva 2 N n N Q n M n Base R Q 2 M 2 Base R
61 55 35 60 sylancr R Ring Q = 1 2 2 1 M B Q 2 M 2 Base R
62 58 42 fvmptg 2 N Q 2 M 2 Base R n N Q n M n 2 = Q 2 M 2
63 55 61 62 sylancr R Ring Q = 1 2 2 1 M B n N Q n M n 2 = Q 2 M 2
64 fveq1 Q = 1 2 2 1 Q 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 Q = 1 2 2 1 Q 2 = 1
68 67 3ad2ant2 R Ring Q = 1 2 2 1 M B Q 2 = 1
69 68 oveq1d R Ring Q = 1 2 2 1 M B Q 2 M 2 = 1 M 2
70 63 69 eqtrd R Ring Q = 1 2 2 1 M B n N Q n M n 2 = 1 M 2
71 53 70 oveq12d R Ring Q = 1 2 2 1 M B n N Q n M n 1 · ˙ n N Q n M n 2 = 2 M 1 · ˙ 1 M 2
72 31 71 eqtrd R Ring Q = 1 2 2 1 M B G n N Q n M n = 2 M 1 · ˙ 1 M 2