Metamath Proof Explorer


Theorem oeeui

Description: The division algorithm for ordinal exponentiation. (This version of oeeu gives an explicit expression for the unique solution of the equation, in terms of the solution P to omeu .) (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Hypotheses oeeu.1 X=xOn|BA𝑜x
oeeu.2 P=ιw|yOnzA𝑜Xw=yzA𝑜X𝑜y+𝑜z=B
oeeu.3 Y=1stP
oeeu.4 Z=2ndP
Assertion oeeui AOn2𝑜BOn1𝑜COnDA1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XD=YE=Z

Proof

Step Hyp Ref Expression
1 oeeu.1 X=xOn|BA𝑜x
2 oeeu.2 P=ιw|yOnzA𝑜Xw=yzA𝑜X𝑜y+𝑜z=B
3 oeeu.3 Y=1stP
4 oeeu.4 Z=2ndP
5 eldifi AOn2𝑜AOn
6 5 adantr AOn2𝑜BOn1𝑜AOn
7 6 ad2antrr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜AOn
8 simprl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜COn
9 oecl AOnCOnA𝑜COn
10 7 8 9 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜COn
11 om1 A𝑜COnA𝑜C𝑜1𝑜=A𝑜C
12 10 11 syl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C𝑜1𝑜=A𝑜C
13 df1o2 1𝑜=
14 dif1o DA1𝑜DAD
15 14 simprbi DA1𝑜D
16 15 ad2antll AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜D
17 eldifi DA1𝑜DA
18 17 ad2antll AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜DA
19 onelon AOnDADOn
20 7 18 19 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜DOn
21 on0eln0 DOnDD
22 20 21 syl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜DD
23 16 22 mpbird AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜D
24 23 snssd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜D
25 13 24 eqsstrid AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜1𝑜D
26 1on 1𝑜On
27 26 a1i AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜1𝑜On
28 omwordi 1𝑜OnDOnA𝑜COn1𝑜DA𝑜C𝑜1𝑜A𝑜C𝑜D
29 27 20 10 28 syl3anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜1𝑜DA𝑜C𝑜1𝑜A𝑜C𝑜D
30 25 29 mpd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C𝑜1𝑜A𝑜C𝑜D
31 12 30 eqsstrrd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜CA𝑜C𝑜D
32 omcl A𝑜COnDOnA𝑜C𝑜DOn
33 10 20 32 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C𝑜DOn
34 simplrl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜EA𝑜C
35 onelon A𝑜COnEA𝑜CEOn
36 10 34 35 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜EOn
37 oaword1 A𝑜C𝑜DOnEOnA𝑜C𝑜DA𝑜C𝑜D+𝑜E
38 33 36 37 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C𝑜DA𝑜C𝑜D+𝑜E
39 simplrr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C𝑜D+𝑜E=B
40 38 39 sseqtrd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C𝑜DB
41 31 40 sstrd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜CB
42 1 oeeulem AOn2𝑜BOn1𝑜XOnA𝑜XBBA𝑜sucX
43 42 simp3d AOn2𝑜BOn1𝑜BA𝑜sucX
44 43 ad2antrr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜BA𝑜sucX
45 42 simp1d AOn2𝑜BOn1𝑜XOn
46 45 ad2antrr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜XOn
47 suceloni XOnsucXOn
48 46 47 syl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜sucXOn
49 oecl AOnsucXOnA𝑜sucXOn
50 7 48 49 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜sucXOn
51 ontr2 A𝑜COnA𝑜sucXOnA𝑜CBBA𝑜sucXA𝑜CA𝑜sucX
52 10 50 51 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜CBBA𝑜sucXA𝑜CA𝑜sucX
53 41 44 52 mp2and AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜CA𝑜sucX
54 simplll AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜AOn2𝑜
55 oeord COnsucXOnAOn2𝑜CsucXA𝑜CA𝑜sucX
56 8 48 54 55 syl3anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜CsucXA𝑜CA𝑜sucX
57 53 56 mpbird AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜CsucX
58 onsssuc COnXOnCXCsucX
59 8 46 58 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜CXCsucX
60 57 59 mpbird AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜CX
61 42 simp2d AOn2𝑜BOn1𝑜A𝑜XB
62 61 ad2antrr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜XB
63 eloni AOnOrdA
64 7 63 syl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜OrdA
65 ordsucss OrdADAsucDA
66 64 18 65 sylc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜sucDA
67 suceloni DOnsucDOn
68 20 67 syl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜sucDOn
69 dif20el AOn2𝑜A
70 54 69 syl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A
71 oen0 AOnCOnAA𝑜C
72 7 8 70 71 syl21anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C
73 omword sucDOnAOnA𝑜COnA𝑜CsucDAA𝑜C𝑜sucDA𝑜C𝑜A
74 68 7 10 72 73 syl31anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜sucDAA𝑜C𝑜sucDA𝑜C𝑜A
75 66 74 mpbid AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C𝑜sucDA𝑜C𝑜A
76 oaord EOnA𝑜COnA𝑜C𝑜DOnEA𝑜CA𝑜C𝑜D+𝑜EA𝑜C𝑜D+𝑜A𝑜C
77 36 10 33 76 syl3anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜EA𝑜CA𝑜C𝑜D+𝑜EA𝑜C𝑜D+𝑜A𝑜C
78 34 77 mpbid AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C𝑜D+𝑜EA𝑜C𝑜D+𝑜A𝑜C
79 39 78 eqeltrrd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜BA𝑜C𝑜D+𝑜A𝑜C
80 odi A𝑜COnDOn1𝑜OnA𝑜C𝑜D+𝑜1𝑜=A𝑜C𝑜D+𝑜A𝑜C𝑜1𝑜
81 10 20 27 80 syl3anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C𝑜D+𝑜1𝑜=A𝑜C𝑜D+𝑜A𝑜C𝑜1𝑜
82 oa1suc DOnD+𝑜1𝑜=sucD
83 20 82 syl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜D+𝑜1𝑜=sucD
84 83 oveq2d AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C𝑜D+𝑜1𝑜=A𝑜C𝑜sucD
85 12 oveq2d AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C𝑜D+𝑜A𝑜C𝑜1𝑜=A𝑜C𝑜D+𝑜A𝑜C
86 81 84 85 3eqtr3d AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜C𝑜sucD=A𝑜C𝑜D+𝑜A𝑜C
87 79 86 eleqtrrd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜BA𝑜C𝑜sucD
88 75 87 sseldd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜BA𝑜C𝑜A
89 oesuc AOnCOnA𝑜sucC=A𝑜C𝑜A
90 7 8 89 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜sucC=A𝑜C𝑜A
91 88 90 eleqtrrd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜BA𝑜sucC
92 oecl AOnXOnA𝑜XOn
93 7 46 92 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜XOn
94 suceloni COnsucCOn
95 94 ad2antrl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜sucCOn
96 oecl AOnsucCOnA𝑜sucCOn
97 7 95 96 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜sucCOn
98 ontr2 A𝑜XOnA𝑜sucCOnA𝑜XBBA𝑜sucCA𝑜XA𝑜sucC
99 93 97 98 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜XBBA𝑜sucCA𝑜XA𝑜sucC
100 62 91 99 mp2and AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜A𝑜XA𝑜sucC
101 oeord XOnsucCOnAOn2𝑜XsucCA𝑜XA𝑜sucC
102 46 95 54 101 syl3anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜XsucCA𝑜XA𝑜sucC
103 100 102 mpbird AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜XsucC
104 onsssuc XOnCOnXCXsucC
105 46 8 104 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜XCXsucC
106 103 105 mpbird AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜XC
107 60 106 eqssd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜C=X
108 107 20 jca AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜C=XDOn
109 simprl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnC=X
110 45 ad2antrr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnXOn
111 109 110 eqeltrd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnCOn
112 6 ad2antrr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnAOn
113 112 111 9 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜COn
114 simprr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnDOn
115 113 114 32 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C𝑜DOn
116 simplrl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnEA𝑜C
117 113 116 35 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnEOn
118 115 117 37 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C𝑜DA𝑜C𝑜D+𝑜E
119 simplrr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C𝑜D+𝑜E=B
120 118 119 sseqtrd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C𝑜DB
121 43 ad2antrr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnBA𝑜sucX
122 suceq C=XsucC=sucX
123 122 ad2antrl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnsucC=sucX
124 123 oveq2d AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜sucC=A𝑜sucX
125 112 111 89 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜sucC=A𝑜C𝑜A
126 124 125 eqtr3d AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜sucX=A𝑜C𝑜A
127 121 126 eleqtrd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnBA𝑜C𝑜A
128 omcl A𝑜COnAOnA𝑜C𝑜AOn
129 113 112 128 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C𝑜AOn
130 ontr2 A𝑜C𝑜DOnA𝑜C𝑜AOnA𝑜C𝑜DBBA𝑜C𝑜AA𝑜C𝑜DA𝑜C𝑜A
131 115 129 130 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C𝑜DBBA𝑜C𝑜AA𝑜C𝑜DA𝑜C𝑜A
132 120 127 131 mp2and AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C𝑜DA𝑜C𝑜A
133 69 adantr AOn2𝑜BOn1𝑜A
134 133 ad2antrr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA
135 112 111 134 71 syl21anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C
136 omord2 DOnAOnA𝑜COnA𝑜CDAA𝑜C𝑜DA𝑜C𝑜A
137 114 112 113 135 136 syl31anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnDAA𝑜C𝑜DA𝑜C𝑜A
138 132 137 mpbird AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnDA
139 109 oveq2d AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C=A𝑜X
140 61 ad2antrr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜XB
141 139 140 eqsstrd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜CB
142 eldifi BOn1𝑜BOn
143 142 adantl AOn2𝑜BOn1𝑜BOn
144 143 ad2antrr AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnBOn
145 ontri1 A𝑜COnBOnA𝑜CB¬BA𝑜C
146 113 144 145 syl2anc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜CB¬BA𝑜C
147 141 146 mpbid AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOn¬BA𝑜C
148 om0 A𝑜COnA𝑜C𝑜=
149 113 148 syl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C𝑜=
150 149 oveq1d AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C𝑜+𝑜E=+𝑜E
151 oa0r EOn+𝑜E=E
152 117 151 syl AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOn+𝑜E=E
153 150 152 eqtrd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C𝑜+𝑜E=E
154 153 116 eqeltrd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C𝑜+𝑜EA𝑜C
155 oveq2 D=A𝑜C𝑜D=A𝑜C𝑜
156 155 oveq1d D=A𝑜C𝑜D+𝑜E=A𝑜C𝑜+𝑜E
157 156 eleq1d D=A𝑜C𝑜D+𝑜EA𝑜CA𝑜C𝑜+𝑜EA𝑜C
158 154 157 syl5ibrcom AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnD=A𝑜C𝑜D+𝑜EA𝑜C
159 119 eleq1d AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnA𝑜C𝑜D+𝑜EA𝑜CBA𝑜C
160 158 159 sylibd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnD=BA𝑜C
161 160 necon3bd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOn¬BA𝑜CD
162 147 161 mpd AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnD
163 138 162 14 sylanbrc AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnDA1𝑜
164 111 163 jca AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnCOnDA1𝑜
165 108 164 impbida AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜C=XDOn
166 165 ex AOn2𝑜BOn1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜C=XDOn
167 166 pm5.32rd AOn2𝑜BOn1𝑜COnDA1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnEA𝑜CA𝑜C𝑜D+𝑜E=B
168 anass C=XDOnEA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnEA𝑜CA𝑜C𝑜D+𝑜E=B
169 167 168 bitrdi AOn2𝑜BOn1𝑜COnDA1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XDOnEA𝑜CA𝑜C𝑜D+𝑜E=B
170 3anass DOnEA𝑜CA𝑜C𝑜D+𝑜E=BDOnEA𝑜CA𝑜C𝑜D+𝑜E=B
171 oveq2 C=XA𝑜C=A𝑜X
172 171 eleq2d C=XEA𝑜CEA𝑜X
173 171 oveq1d C=XA𝑜C𝑜D=A𝑜X𝑜D
174 173 oveq1d C=XA𝑜C𝑜D+𝑜E=A𝑜X𝑜D+𝑜E
175 174 eqeq1d C=XA𝑜C𝑜D+𝑜E=BA𝑜X𝑜D+𝑜E=B
176 172 175 3anbi23d C=XDOnEA𝑜CA𝑜C𝑜D+𝑜E=BDOnEA𝑜XA𝑜X𝑜D+𝑜E=B
177 170 176 bitr3id C=XDOnEA𝑜CA𝑜C𝑜D+𝑜E=BDOnEA𝑜XA𝑜X𝑜D+𝑜E=B
178 6 45 92 syl2anc AOn2𝑜BOn1𝑜A𝑜XOn
179 oen0 AOnXOnAA𝑜X
180 6 45 133 179 syl21anc AOn2𝑜BOn1𝑜A𝑜X
181 180 ne0d AOn2𝑜BOn1𝑜A𝑜X
182 omeu A𝑜XOnBOnA𝑜X∃!adOneA𝑜Xa=deA𝑜X𝑜d+𝑜e=B
183 opeq1 y=dyz=dz
184 183 eqeq2d y=dw=yzw=dz
185 oveq2 y=dA𝑜X𝑜y=A𝑜X𝑜d
186 185 oveq1d y=dA𝑜X𝑜y+𝑜z=A𝑜X𝑜d+𝑜z
187 186 eqeq1d y=dA𝑜X𝑜y+𝑜z=BA𝑜X𝑜d+𝑜z=B
188 184 187 anbi12d y=dw=yzA𝑜X𝑜y+𝑜z=Bw=dzA𝑜X𝑜d+𝑜z=B
189 opeq2 z=edz=de
190 189 eqeq2d z=ew=dzw=de
191 oveq2 z=eA𝑜X𝑜d+𝑜z=A𝑜X𝑜d+𝑜e
192 191 eqeq1d z=eA𝑜X𝑜d+𝑜z=BA𝑜X𝑜d+𝑜e=B
193 190 192 anbi12d z=ew=dzA𝑜X𝑜d+𝑜z=Bw=deA𝑜X𝑜d+𝑜e=B
194 188 193 cbvrex2vw yOnzA𝑜Xw=yzA𝑜X𝑜y+𝑜z=BdOneA𝑜Xw=deA𝑜X𝑜d+𝑜e=B
195 eqeq1 w=aw=dea=de
196 195 anbi1d w=aw=deA𝑜X𝑜d+𝑜e=Ba=deA𝑜X𝑜d+𝑜e=B
197 196 2rexbidv w=adOneA𝑜Xw=deA𝑜X𝑜d+𝑜e=BdOneA𝑜Xa=deA𝑜X𝑜d+𝑜e=B
198 194 197 bitrid w=ayOnzA𝑜Xw=yzA𝑜X𝑜y+𝑜z=BdOneA𝑜Xa=deA𝑜X𝑜d+𝑜e=B
199 198 cbviotavw ιw|yOnzA𝑜Xw=yzA𝑜X𝑜y+𝑜z=B=ιa|dOneA𝑜Xa=deA𝑜X𝑜d+𝑜e=B
200 2 199 eqtri P=ιa|dOneA𝑜Xa=deA𝑜X𝑜d+𝑜e=B
201 oveq2 d=DA𝑜X𝑜d=A𝑜X𝑜D
202 201 oveq1d d=DA𝑜X𝑜d+𝑜e=A𝑜X𝑜D+𝑜e
203 202 eqeq1d d=DA𝑜X𝑜d+𝑜e=BA𝑜X𝑜D+𝑜e=B
204 oveq2 e=EA𝑜X𝑜D+𝑜e=A𝑜X𝑜D+𝑜E
205 204 eqeq1d e=EA𝑜X𝑜D+𝑜e=BA𝑜X𝑜D+𝑜E=B
206 200 3 4 203 205 opiota ∃!adOneA𝑜Xa=deA𝑜X𝑜d+𝑜e=BDOnEA𝑜XA𝑜X𝑜D+𝑜E=BD=YE=Z
207 182 206 syl A𝑜XOnBOnA𝑜XDOnEA𝑜XA𝑜X𝑜D+𝑜E=BD=YE=Z
208 178 143 181 207 syl3anc AOn2𝑜BOn1𝑜DOnEA𝑜XA𝑜X𝑜D+𝑜E=BD=YE=Z
209 177 208 sylan9bbr AOn2𝑜BOn1𝑜C=XDOnEA𝑜CA𝑜C𝑜D+𝑜E=BD=YE=Z
210 209 pm5.32da AOn2𝑜BOn1𝑜C=XDOnEA𝑜CA𝑜C𝑜D+𝑜E=BC=XD=YE=Z
211 169 210 bitrd AOn2𝑜BOn1𝑜COnDA1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XD=YE=Z
212 3an4anass COnDA1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BCOnDA1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=B
213 3anass C=XD=YE=ZC=XD=YE=Z
214 211 212 213 3bitr4g AOn2𝑜BOn1𝑜COnDA1𝑜EA𝑜CA𝑜C𝑜D+𝑜E=BC=XD=YE=Z