Metamath Proof Explorer


Theorem mdetunilem6

Description: Lemma for mdetuni . (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses mdetuni.a A=NMatR
mdetuni.b B=BaseA
mdetuni.k K=BaseR
mdetuni.0g 0˙=0R
mdetuni.1r 1˙=1R
mdetuni.pg +˙=+R
mdetuni.tg ·˙=R
mdetuni.n φNFin
mdetuni.r φRRing
mdetuni.ff φD:BK
mdetuni.al φxByNzNyzwNyxw=zxwDx=0˙
mdetuni.li φxByBzBwNxw×N=yw×N+˙fzw×NxNw×N=yNw×NxNw×N=zNw×NDx=Dy+˙Dz
mdetuni.sc φxByKzBwNxw×N=w×N×y·˙fzw×NxNw×N=zNw×NDx=y·˙Dz
mdetunilem6.ph ψφ
mdetunilem6.ef ψENFNEF
mdetunilem6.gh ψbNGKHK
mdetunilem6.i ψaNbNIK
Assertion mdetunilem6 ψDaN,bNifa=EGifa=FHI=invgRDaN,bNifa=EHifa=FGI

Proof

Step Hyp Ref Expression
1 mdetuni.a A=NMatR
2 mdetuni.b B=BaseA
3 mdetuni.k K=BaseR
4 mdetuni.0g 0˙=0R
5 mdetuni.1r 1˙=1R
6 mdetuni.pg +˙=+R
7 mdetuni.tg ·˙=R
8 mdetuni.n φNFin
9 mdetuni.r φRRing
10 mdetuni.ff φD:BK
11 mdetuni.al φxByNzNyzwNyxw=zxwDx=0˙
12 mdetuni.li φxByBzBwNxw×N=yw×N+˙fzw×NxNw×N=yNw×NxNw×N=zNw×NDx=Dy+˙Dz
13 mdetuni.sc φxByKzBwNxw×N=w×N×y·˙fzw×NxNw×N=zNw×NDx=y·˙Dz
14 mdetunilem6.ph ψφ
15 mdetunilem6.ef ψENFNEF
16 mdetunilem6.gh ψbNGKHK
17 mdetunilem6.i ψaNbNIK
18 15 simp1d ψEN
19 16 simprd ψbNHK
20 19 3adant2 ψaNbNHK
21 16 simpld ψbNGK
22 21 3adant2 ψaNbNGK
23 ringgrp RRingRGrp
24 14 9 23 3syl ψRGrp
25 24 adantr ψbNRGrp
26 3 6 grpcl RGrpHKGKH+˙GK
27 25 19 21 26 syl3anc ψbNH+˙GK
28 27 3adant2 ψaNbNH+˙GK
29 28 17 ifcld ψaNbNifa=FH+˙GIK
30 20 22 29 3jca ψaNbNHKGKifa=FH+˙GIK
31 1 2 3 4 5 6 7 8 9 10 11 12 13 14 18 30 mdetunilem5 ψDaN,bNifa=EH+˙Gifa=FH+˙GI=DaN,bNifa=EHifa=FH+˙GI+˙DaN,bNifa=EGifa=FH+˙GI
32 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 27 17 mdetunilem2 ψDaN,bNifa=EH+˙Gifa=FH+˙GI=0˙
33 15 simp2d ψFN
34 20 17 ifcld ψaNbNifa=EHIK
35 20 22 34 3jca ψaNbNHKGKifa=EHIK
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 33 35 mdetunilem5 ψDaN,bNifa=FH+˙Gifa=EHI=DaN,bNifa=FHifa=EHI+˙DaN,bNifa=FGifa=EHI
37 15 simp3d ψEF
38 37 necomd ψFE
39 33 18 38 3jca ψFNENFE
40 1 2 3 4 5 6 7 8 9 10 11 12 13 14 39 19 17 mdetunilem2 ψDaN,bNifa=FHifa=EHI=0˙
41 40 oveq1d ψDaN,bNifa=FHifa=EHI+˙DaN,bNifa=FGifa=EHI=0˙+˙DaN,bNifa=FGifa=EHI
42 37 neneqd ψ¬E=F
43 eqtr2 a=Ea=FE=F
44 42 43 nsyl ψ¬a=Ea=F
45 44 3ad2ant1 ψaNbN¬a=Ea=F
46 ifcomnan ¬a=Ea=Fifa=EHifa=FGI=ifa=FGifa=EHI
47 45 46 syl ψaNbNifa=EHifa=FGI=ifa=FGifa=EHI
48 47 mpoeq3dva ψaN,bNifa=EHifa=FGI=aN,bNifa=FGifa=EHI
49 48 fveq2d ψDaN,bNifa=EHifa=FGI=DaN,bNifa=FGifa=EHI
50 14 10 syl ψD:BK
51 14 8 syl ψNFin
52 22 17 ifcld ψaNbNifa=FGIK
53 20 52 ifcld ψaNbNifa=EHifa=FGIK
54 1 3 2 51 24 53 matbas2d ψaN,bNifa=EHifa=FGIB
55 50 54 ffvelrnd ψDaN,bNifa=EHifa=FGIK
56 49 55 eqeltrrd ψDaN,bNifa=FGifa=EHIK
57 3 6 4 grplid RGrpDaN,bNifa=FGifa=EHIK0˙+˙DaN,bNifa=FGifa=EHI=DaN,bNifa=FGifa=EHI
58 24 56 57 syl2anc ψ0˙+˙DaN,bNifa=FGifa=EHI=DaN,bNifa=FGifa=EHI
59 36 41 58 3eqtrd ψDaN,bNifa=FH+˙Gifa=EHI=DaN,bNifa=FGifa=EHI
60 ifcomnan ¬a=Ea=Fifa=EHifa=FH+˙GI=ifa=FH+˙Gifa=EHI
61 45 60 syl ψaNbNifa=EHifa=FH+˙GI=ifa=FH+˙Gifa=EHI
62 61 mpoeq3dva ψaN,bNifa=EHifa=FH+˙GI=aN,bNifa=FH+˙Gifa=EHI
63 62 fveq2d ψDaN,bNifa=EHifa=FH+˙GI=DaN,bNifa=FH+˙Gifa=EHI
64 59 63 49 3eqtr4d ψDaN,bNifa=EHifa=FH+˙GI=DaN,bNifa=EHifa=FGI
65 22 17 ifcld ψaNbNifa=EGIK
66 20 22 65 3jca ψaNbNHKGKifa=EGIK
67 1 2 3 4 5 6 7 8 9 10 11 12 13 14 33 66 mdetunilem5 ψDaN,bNifa=FH+˙Gifa=EGI=DaN,bNifa=FHifa=EGI+˙DaN,bNifa=FGifa=EGI
68 1 2 3 4 5 6 7 8 9 10 11 12 13 14 39 21 17 mdetunilem2 ψDaN,bNifa=FGifa=EGI=0˙
69 68 oveq2d ψDaN,bNifa=FHifa=EGI+˙DaN,bNifa=FGifa=EGI=DaN,bNifa=FHifa=EGI+˙0˙
70 ifcomnan ¬a=Ea=Fifa=EGifa=FHI=ifa=FHifa=EGI
71 45 70 syl ψaNbNifa=EGifa=FHI=ifa=FHifa=EGI
72 71 mpoeq3dva ψaN,bNifa=EGifa=FHI=aN,bNifa=FHifa=EGI
73 72 fveq2d ψDaN,bNifa=EGifa=FHI=DaN,bNifa=FHifa=EGI
74 20 17 ifcld ψaNbNifa=FHIK
75 22 74 ifcld ψaNbNifa=EGifa=FHIK
76 1 3 2 51 24 75 matbas2d ψaN,bNifa=EGifa=FHIB
77 50 76 ffvelrnd ψDaN,bNifa=EGifa=FHIK
78 73 77 eqeltrrd ψDaN,bNifa=FHifa=EGIK
79 3 6 4 grprid RGrpDaN,bNifa=FHifa=EGIKDaN,bNifa=FHifa=EGI+˙0˙=DaN,bNifa=FHifa=EGI
80 24 78 79 syl2anc ψDaN,bNifa=FHifa=EGI+˙0˙=DaN,bNifa=FHifa=EGI
81 67 69 80 3eqtrd ψDaN,bNifa=FH+˙Gifa=EGI=DaN,bNifa=FHifa=EGI
82 ifcomnan ¬a=Ea=Fifa=EGifa=FH+˙GI=ifa=FH+˙Gifa=EGI
83 45 82 syl ψaNbNifa=EGifa=FH+˙GI=ifa=FH+˙Gifa=EGI
84 83 mpoeq3dva ψaN,bNifa=EGifa=FH+˙GI=aN,bNifa=FH+˙Gifa=EGI
85 84 fveq2d ψDaN,bNifa=EGifa=FH+˙GI=DaN,bNifa=FH+˙Gifa=EGI
86 81 85 73 3eqtr4d ψDaN,bNifa=EGifa=FH+˙GI=DaN,bNifa=EGifa=FHI
87 64 86 oveq12d ψDaN,bNifa=EHifa=FH+˙GI+˙DaN,bNifa=EGifa=FH+˙GI=DaN,bNifa=EHifa=FGI+˙DaN,bNifa=EGifa=FHI
88 31 32 87 3eqtr3rd ψDaN,bNifa=EHifa=FGI+˙DaN,bNifa=EGifa=FHI=0˙
89 eqid invgR=invgR
90 3 6 4 89 grpinvid1 RGrpDaN,bNifa=EHifa=FGIKDaN,bNifa=EGifa=FHIKinvgRDaN,bNifa=EHifa=FGI=DaN,bNifa=EGifa=FHIDaN,bNifa=EHifa=FGI+˙DaN,bNifa=EGifa=FHI=0˙
91 24 55 77 90 syl3anc ψinvgRDaN,bNifa=EHifa=FGI=DaN,bNifa=EGifa=FHIDaN,bNifa=EHifa=FGI+˙DaN,bNifa=EGifa=FHI=0˙
92 88 91 mpbird ψinvgRDaN,bNifa=EHifa=FGI=DaN,bNifa=EGifa=FHI
93 92 eqcomd ψDaN,bNifa=EGifa=FHI=invgRDaN,bNifa=EHifa=FGI