Metamath Proof Explorer


Theorem cayhamlem2

Description: Lemma for cayhamlem3 . (Contributed by AV, 24-Nov-2019)

Ref Expression
Hypotheses cayhamlem2.k K=BaseR
cayhamlem2.a A=NMatR
cayhamlem2.b B=BaseA
cayhamlem2.1 1˙=1A
cayhamlem2.m ˙=A
cayhamlem2.e ×˙=mulGrpA
cayhamlem2.r ·˙=A
Assertion cayhamlem2 NFinRCRingMBHK0L0HL˙L×˙M=L×˙M·˙HL˙1˙

Proof

Step Hyp Ref Expression
1 cayhamlem2.k K=BaseR
2 cayhamlem2.a A=NMatR
3 cayhamlem2.b B=BaseA
4 cayhamlem2.1 1˙=1A
5 cayhamlem2.m ˙=A
6 cayhamlem2.e ×˙=mulGrpA
7 cayhamlem2.r ·˙=A
8 elmapi HK0H:0K
9 8 ffvelcdmda HK0L0HLK
10 9 adantl NFinRCRingMBHK0L0HLK
11 2 matsca2 NFinRCRingR=ScalarA
12 11 3adant3 NFinRCRingMBR=ScalarA
13 12 fveq2d NFinRCRingMBBaseR=BaseScalarA
14 1 13 eqtr2id NFinRCRingMBBaseScalarA=K
15 14 eleq2d NFinRCRingMBHLBaseScalarAHLK
16 15 adantr NFinRCRingMBHK0L0HLBaseScalarAHLK
17 10 16 mpbird NFinRCRingMBHK0L0HLBaseScalarA
18 eqid algScA=algScA
19 eqid ScalarA=ScalarA
20 eqid BaseScalarA=BaseScalarA
21 18 19 20 5 4 asclval HLBaseScalarAalgScAHL=HL˙1˙
22 17 21 syl NFinRCRingMBHK0L0algScAHL=HL˙1˙
23 22 eqcomd NFinRCRingMBHK0L0HL˙1˙=algScAHL
24 23 oveq2d NFinRCRingMBHK0L0L×˙M·˙HL˙1˙=L×˙M·˙algScAHL
25 2 matassa NFinRCRingAAssAlg
26 25 3adant3 NFinRCRingMBAAssAlg
27 26 adantr NFinRCRingMBHK0L0AAssAlg
28 eqid mulGrpA=mulGrpA
29 28 3 mgpbas B=BasemulGrpA
30 crngring RCRingRRing
31 30 anim2i NFinRCRingNFinRRing
32 31 3adant3 NFinRCRingMBNFinRRing
33 2 matring NFinRRingARing
34 28 ringmgp ARingmulGrpAMnd
35 32 33 34 3syl NFinRCRingMBmulGrpAMnd
36 35 adantr NFinRCRingMBHK0L0mulGrpAMnd
37 simprr NFinRCRingMBHK0L0L0
38 simpl3 NFinRCRingMBHK0L0MB
39 29 6 36 37 38 mulgnn0cld NFinRCRingMBHK0L0L×˙MB
40 18 19 20 3 7 5 asclmul2 AAssAlgHLBaseScalarAL×˙MBL×˙M·˙algScAHL=HL˙L×˙M
41 27 17 39 40 syl3anc NFinRCRingMBHK0L0L×˙M·˙algScAHL=HL˙L×˙M
42 24 41 eqtr2d NFinRCRingMBHK0L0HL˙L×˙M=L×˙M·˙HL˙1˙