Metamath Proof Explorer

Theorem oaomoencom

Description: Ordinal addition, multiplication, and exponentiation do not generally commute. Theorem 4.1 of Schloeder p. 11. (Contributed by RP, 30-Jan-2025)

Ref Expression
Assertion oaomoencom 
|- ( E. a e. On E. b e. On -. ( a +o b ) = ( b +o a ) /\ E. a e. On E. b e. On -. ( a .o b ) = ( b .o a ) /\ E. a e. On E. b e. On -. ( a ^o b ) = ( b ^o a ) )

Proof

Step Hyp Ref Expression
1 oancom 
 |-  ( 1o +o _om ) =/= ( _om +o 1o )
2 1 neii 
 |-  -. ( 1o +o _om ) = ( _om +o 1o )
3 1on 
 |-  1o e. On
4 omelon 
 |-  _om e. On
5 oveq2 
 |-  ( b = _om -> ( 1o +o b ) = ( 1o +o _om ) )
6 oveq1 
 |-  ( b = _om -> ( b +o 1o ) = ( _om +o 1o ) )
7 5 6 eqeq12d 
 |-  ( b = _om -> ( ( 1o +o b ) = ( b +o 1o ) <-> ( 1o +o _om ) = ( _om +o 1o ) ) )
8 7 notbid 
 |-  ( b = _om -> ( -. ( 1o +o b ) = ( b +o 1o ) <-> -. ( 1o +o _om ) = ( _om +o 1o ) ) )
9 8 rspcev 
 |-  ( ( _om e. On /\ -. ( 1o +o _om ) = ( _om +o 1o ) ) -> E. b e. On -. ( 1o +o b ) = ( b +o 1o ) )
10 4 9 mpan 
 |-  ( -. ( 1o +o _om ) = ( _om +o 1o ) -> E. b e. On -. ( 1o +o b ) = ( b +o 1o ) )
11 oveq1 
 |-  ( a = 1o -> ( a +o b ) = ( 1o +o b ) )
12 oveq2 
 |-  ( a = 1o -> ( b +o a ) = ( b +o 1o ) )
13 11 12 eqeq12d 
 |-  ( a = 1o -> ( ( a +o b ) = ( b +o a ) <-> ( 1o +o b ) = ( b +o 1o ) ) )
14 13 notbid 
 |-  ( a = 1o -> ( -. ( a +o b ) = ( b +o a ) <-> -. ( 1o +o b ) = ( b +o 1o ) ) )
15 14 rexbidv 
 |-  ( a = 1o -> ( E. b e. On -. ( a +o b ) = ( b +o a ) <-> E. b e. On -. ( 1o +o b ) = ( b +o 1o ) ) )
16 15 rspcev 
 |-  ( ( 1o e. On /\ E. b e. On -. ( 1o +o b ) = ( b +o 1o ) ) -> E. a e. On E. b e. On -. ( a +o b ) = ( b +o a ) )
17 3 10 16 sylancr 
 |-  ( -. ( 1o +o _om ) = ( _om +o 1o ) -> E. a e. On E. b e. On -. ( a +o b ) = ( b +o a ) )
18 2 17 ax-mp 
 |-  E. a e. On E. b e. On -. ( a +o b ) = ( b +o a )
19 4 4 pm3.2i 
 |-  ( _om e. On /\ _om e. On )
20 peano1 
 |-  (/) e. _om
21 19 20 pm3.2i 
 |-  ( ( _om e. On /\ _om e. On ) /\ (/) e. _om )
22 oaord1 
 |-  ( ( _om e. On /\ _om e. On ) -> ( (/) e. _om <-> _om e. ( _om +o _om ) ) )
23 22 biimpa 
 |-  ( ( ( _om e. On /\ _om e. On ) /\ (/) e. _om ) -> _om e. ( _om +o _om ) )
24 elneq 
 |-  ( _om e. ( _om +o _om ) -> _om =/= ( _om +o _om ) )
25 21 23 24 mp2b 
 |-  _om =/= ( _om +o _om )
26 2omomeqom 
 |-  ( 2o .o _om ) = _om
27 df-2o 
 |-  2o = suc 1o
28 27 oveq2i 
 |-  ( _om .o 2o ) = ( _om .o suc 1o )
29 omsuc 
 |-  ( ( _om e. On /\ 1o e. On ) -> ( _om .o suc 1o ) = ( ( _om .o 1o ) +o _om ) )
30 4 3 29 mp2an 
 |-  ( _om .o suc 1o ) = ( ( _om .o 1o ) +o _om )
31 om1 
 |-  ( _om e. On -> ( _om .o 1o ) = _om )
32 4 31 ax-mp 
 |-  ( _om .o 1o ) = _om
33 32 oveq1i 
 |-  ( ( _om .o 1o ) +o _om ) = ( _om +o _om )
34 28 30 33 3eqtri 
 |-  ( _om .o 2o ) = ( _om +o _om )
35 26 34 neeq12i 
 |-  ( ( 2o .o _om ) =/= ( _om .o 2o ) <-> _om =/= ( _om +o _om ) )
36 25 35 mpbir 
 |-  ( 2o .o _om ) =/= ( _om .o 2o )
37 36 neii 
 |-  -. ( 2o .o _om ) = ( _om .o 2o )
38 2on 
 |-  2o e. On
39 oveq2 
 |-  ( b = _om -> ( 2o .o b ) = ( 2o .o _om ) )
40 oveq1 
 |-  ( b = _om -> ( b .o 2o ) = ( _om .o 2o ) )
41 39 40 eqeq12d 
 |-  ( b = _om -> ( ( 2o .o b ) = ( b .o 2o ) <-> ( 2o .o _om ) = ( _om .o 2o ) ) )
42 41 notbid 
 |-  ( b = _om -> ( -. ( 2o .o b ) = ( b .o 2o ) <-> -. ( 2o .o _om ) = ( _om .o 2o ) ) )
43 42 rspcev 
 |-  ( ( _om e. On /\ -. ( 2o .o _om ) = ( _om .o 2o ) ) -> E. b e. On -. ( 2o .o b ) = ( b .o 2o ) )
44 4 43 mpan 
 |-  ( -. ( 2o .o _om ) = ( _om .o 2o ) -> E. b e. On -. ( 2o .o b ) = ( b .o 2o ) )
45 oveq1 
 |-  ( a = 2o -> ( a .o b ) = ( 2o .o b ) )
46 oveq2 
 |-  ( a = 2o -> ( b .o a ) = ( b .o 2o ) )
47 45 46 eqeq12d 
 |-  ( a = 2o -> ( ( a .o b ) = ( b .o a ) <-> ( 2o .o b ) = ( b .o 2o ) ) )
48 47 notbid 
 |-  ( a = 2o -> ( -. ( a .o b ) = ( b .o a ) <-> -. ( 2o .o b ) = ( b .o 2o ) ) )
49 48 rexbidv 
 |-  ( a = 2o -> ( E. b e. On -. ( a .o b ) = ( b .o a ) <-> E. b e. On -. ( 2o .o b ) = ( b .o 2o ) ) )
50 49 rspcev 
 |-  ( ( 2o e. On /\ E. b e. On -. ( 2o .o b ) = ( b .o 2o ) ) -> E. a e. On E. b e. On -. ( a .o b ) = ( b .o a ) )
51 38 44 50 sylancr 
 |-  ( -. ( 2o .o _om ) = ( _om .o 2o ) -> E. a e. On E. b e. On -. ( a .o b ) = ( b .o a ) )
52 37 51 ax-mp 
 |-  E. a e. On E. b e. On -. ( a .o b ) = ( b .o a )
53 1onn 
 |-  1o e. _om
54 21 53 pm3.2i 
 |-  ( ( ( _om e. On /\ _om e. On ) /\ (/) e. _om ) /\ 1o e. _om )
55 4 31 mp1i 
 |-  ( ( ( ( _om e. On /\ _om e. On ) /\ (/) e. _om ) /\ 1o e. _om ) -> ( _om .o 1o ) = _om )
56 omordi 
 |-  ( ( ( _om e. On /\ _om e. On ) /\ (/) e. _om ) -> ( 1o e. _om -> ( _om .o 1o ) e. ( _om .o _om ) ) )
57 56 imp 
 |-  ( ( ( ( _om e. On /\ _om e. On ) /\ (/) e. _om ) /\ 1o e. _om ) -> ( _om .o 1o ) e. ( _om .o _om ) )
58 55 57 eqeltrrd 
 |-  ( ( ( ( _om e. On /\ _om e. On ) /\ (/) e. _om ) /\ 1o e. _om ) -> _om e. ( _om .o _om ) )
59 elneq 
 |-  ( _om e. ( _om .o _om ) -> _om =/= ( _om .o _om ) )
60 54 58 59 mp2b 
 |-  _om =/= ( _om .o _om )
61 2onn 
 |-  2o e. _om
62 1oex 
 |-  1o e. _V
63 62 prid2 
 |-  1o e. { (/) , 1o }
64 df2o3 
 |-  2o = { (/) , 1o }
65 63 64 eleqtrri 
 |-  1o e. 2o
66 nnoeomeqom 
 |-  ( ( 2o e. _om /\ 1o e. 2o ) -> ( 2o ^o _om ) = _om )
67 61 65 66 mp2an 
 |-  ( 2o ^o _om ) = _om
68 27 oveq2i 
 |-  ( _om ^o 2o ) = ( _om ^o suc 1o )
69 oesuc 
 |-  ( ( _om e. On /\ 1o e. On ) -> ( _om ^o suc 1o ) = ( ( _om ^o 1o ) .o _om ) )
70 4 3 69 mp2an 
 |-  ( _om ^o suc 1o ) = ( ( _om ^o 1o ) .o _om )
71 oe1 
 |-  ( _om e. On -> ( _om ^o 1o ) = _om )
72 4 71 ax-mp 
 |-  ( _om ^o 1o ) = _om
73 72 oveq1i 
 |-  ( ( _om ^o 1o ) .o _om ) = ( _om .o _om )
74 68 70 73 3eqtri 
 |-  ( _om ^o 2o ) = ( _om .o _om )
75 67 74 neeq12i 
 |-  ( ( 2o ^o _om ) =/= ( _om ^o 2o ) <-> _om =/= ( _om .o _om ) )
76 60 75 mpbir 
 |-  ( 2o ^o _om ) =/= ( _om ^o 2o )
77 76 neii 
 |-  -. ( 2o ^o _om ) = ( _om ^o 2o )
78 oveq2 
 |-  ( b = _om -> ( 2o ^o b ) = ( 2o ^o _om ) )
79 oveq1 
 |-  ( b = _om -> ( b ^o 2o ) = ( _om ^o 2o ) )
80 78 79 eqeq12d 
 |-  ( b = _om -> ( ( 2o ^o b ) = ( b ^o 2o ) <-> ( 2o ^o _om ) = ( _om ^o 2o ) ) )
81 80 notbid 
 |-  ( b = _om -> ( -. ( 2o ^o b ) = ( b ^o 2o ) <-> -. ( 2o ^o _om ) = ( _om ^o 2o ) ) )
82 81 rspcev 
 |-  ( ( _om e. On /\ -. ( 2o ^o _om ) = ( _om ^o 2o ) ) -> E. b e. On -. ( 2o ^o b ) = ( b ^o 2o ) )
83 4 82 mpan 
 |-  ( -. ( 2o ^o _om ) = ( _om ^o 2o ) -> E. b e. On -. ( 2o ^o b ) = ( b ^o 2o ) )
84 oveq1 
 |-  ( a = 2o -> ( a ^o b ) = ( 2o ^o b ) )
85 oveq2 
 |-  ( a = 2o -> ( b ^o a ) = ( b ^o 2o ) )
86 84 85 eqeq12d 
 |-  ( a = 2o -> ( ( a ^o b ) = ( b ^o a ) <-> ( 2o ^o b ) = ( b ^o 2o ) ) )
87 86 notbid 
 |-  ( a = 2o -> ( -. ( a ^o b ) = ( b ^o a ) <-> -. ( 2o ^o b ) = ( b ^o 2o ) ) )
88 87 rexbidv 
 |-  ( a = 2o -> ( E. b e. On -. ( a ^o b ) = ( b ^o a ) <-> E. b e. On -. ( 2o ^o b ) = ( b ^o 2o ) ) )
89 88 rspcev 
 |-  ( ( 2o e. On /\ E. b e. On -. ( 2o ^o b ) = ( b ^o 2o ) ) -> E. a e. On E. b e. On -. ( a ^o b ) = ( b ^o a ) )
90 38 83 89 sylancr 
 |-  ( -. ( 2o ^o _om ) = ( _om ^o 2o ) -> E. a e. On E. b e. On -. ( a ^o b ) = ( b ^o a ) )
91 77 90 ax-mp 
 |-  E. a e. On E. b e. On -. ( a ^o b ) = ( b ^o a )
92 18 52 91 3pm3.2i 
 |-  ( E. a e. On E. b e. On -. ( a +o b ) = ( b +o a ) /\ E. a e. On E. b e. On -. ( a .o b ) = ( b .o a ) /\ E. a e. On E. b e. On -. ( a ^o b ) = ( b ^o a ) )