Metamath Proof Explorer


Theorem remullem

Description: Lemma for remul , immul , and cjmul . (Contributed by NM, 28-Jul-1999) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion remullem ABAB=ABABAB=AB+ABAB=AB

Proof

Step Hyp Ref Expression
1 replim AA=A+iA
2 replim BB=B+iB
3 1 2 oveqan12d ABAB=A+iAB+iB
4 recl AA
5 4 adantr ABA
6 5 recnd ABA
7 ax-icn i
8 imcl AA
9 8 adantr ABA
10 9 recnd ABA
11 mulcl iAiA
12 7 10 11 sylancr ABiA
13 6 12 addcld ABA+iA
14 recl BB
15 14 adantl ABB
16 15 recnd ABB
17 imcl BB
18 17 adantl ABB
19 18 recnd ABB
20 mulcl iBiB
21 7 19 20 sylancr ABiB
22 13 16 21 adddid ABA+iAB+iB=A+iAB+A+iAiB
23 6 12 16 adddird ABA+iAB=AB+iAB
24 6 12 21 adddird ABA+iAiB=AiB+iAiB
25 23 24 oveq12d ABA+iAB+A+iAiB=AB+iAB+AiB+iAiB
26 5 15 remulcld ABAB
27 26 recnd ABAB
28 12 21 mulcld ABiAiB
29 12 16 mulcld ABiAB
30 6 21 mulcld ABAiB
31 27 28 29 30 add42d ABAB+iAiB+iAB+AiB=AB+iAB+AiB+iAiB
32 7 a1i ABi
33 32 10 32 19 mul4d ABiAiB=iiAB
34 ixi ii=1
35 34 oveq1i iiAB=-1AB
36 9 18 remulcld ABAB
37 36 recnd ABAB
38 37 mulm1d AB-1AB=AB
39 35 38 eqtrid ABiiAB=AB
40 33 39 eqtrd ABiAiB=AB
41 40 oveq2d ABAB+iAiB=AB+AB
42 27 37 negsubd ABAB+AB=ABAB
43 41 42 eqtrd ABAB+iAiB=ABAB
44 9 15 remulcld ABAB
45 44 recnd ABAB
46 mulcl iABiAB
47 7 45 46 sylancr ABiAB
48 5 18 remulcld ABAB
49 48 recnd ABAB
50 mulcl iABiAB
51 7 49 50 sylancr ABiAB
52 47 51 addcomd ABiAB+iAB=iAB+iAB
53 32 10 16 mulassd ABiAB=iAB
54 6 32 19 mul12d ABAiB=iAB
55 53 54 oveq12d ABiAB+AiB=iAB+iAB
56 32 49 45 adddid ABiAB+AB=iAB+iAB
57 52 55 56 3eqtr4d ABiAB+AiB=iAB+AB
58 43 57 oveq12d ABAB+iAiB+iAB+AiB=AB-AB+iAB+AB
59 25 31 58 3eqtr2d ABA+iAB+A+iAiB=AB-AB+iAB+AB
60 3 22 59 3eqtrd ABAB=AB-AB+iAB+AB
61 60 fveq2d ABAB=AB-AB+iAB+AB
62 26 36 resubcld ABABAB
63 48 44 readdcld ABAB+AB
64 crre ABABAB+ABAB-AB+iAB+AB=ABAB
65 62 63 64 syl2anc ABAB-AB+iAB+AB=ABAB
66 61 65 eqtrd ABAB=ABAB
67 60 fveq2d ABAB=AB-AB+iAB+AB
68 crim ABABAB+ABAB-AB+iAB+AB=AB+AB
69 62 63 68 syl2anc ABAB-AB+iAB+AB=AB+AB
70 67 69 eqtrd ABAB=AB+AB
71 mulcl ABAB
72 remim ABAB=ABiAB
73 71 72 syl ABAB=ABiAB
74 remim AA=AiA
75 remim BB=BiB
76 74 75 oveqan12d ABAB=AiABiB
77 16 21 subcld ABBiB
78 6 12 77 subdird ABAiABiB=ABiBiABiB
79 27 30 29 28 subadd4d ABAB-AiB-iABiAiB=AB+iAiB-AiB+iAB
80 6 16 21 subdid ABABiB=ABAiB
81 12 16 21 subdid ABiABiB=iABiAiB
82 80 81 oveq12d ABABiBiABiB=AB-AiB-iABiAiB
83 65 61 43 3eqtr4d ABAB=AB+iAiB
84 70 oveq2d ABiAB=iAB+AB
85 54 53 oveq12d ABAiB+iAB=iAB+iAB
86 56 84 85 3eqtr4d ABiAB=AiB+iAB
87 83 86 oveq12d ABABiAB=AB+iAiB-AiB+iAB
88 79 82 87 3eqtr4d ABABiBiABiB=ABiAB
89 76 78 88 3eqtrd ABAB=ABiAB
90 73 89 eqtr4d ABAB=AB
91 66 70 90 3jca ABAB=ABABAB=AB+ABAB=AB