Metamath Proof Explorer

Theorem oeoa

Description: Sum of exponents law for ordinal exponentiation. Theorem 8R of Enderton p. 238. Also Proposition 8.41 of TakeutiZaring p. 69. Theorem 4.7 of Schloeder p. 14. (Contributed by Eric Schmidt, 26-May-2009)

Ref Expression
Assertion oeoa 
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )

Proof

Step Hyp Ref Expression
1 oa00 
 |-  ( ( B e. On /\ C e. On ) -> ( ( B +o C ) = (/) <-> ( B = (/) /\ C = (/) ) ) )
2 1 biimpar 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( B = (/) /\ C = (/) ) ) -> ( B +o C ) = (/) )
3 2 oveq2d 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( B = (/) /\ C = (/) ) ) -> ( (/) ^o ( B +o C ) ) = ( (/) ^o (/) ) )
4 oveq2 
 |-  ( B = (/) -> ( (/) ^o B ) = ( (/) ^o (/) ) )
5 oveq2 
 |-  ( C = (/) -> ( (/) ^o C ) = ( (/) ^o (/) ) )
6 oe0m0 
 |-  ( (/) ^o (/) ) = 1o
7 5 6 eqtrdi 
 |-  ( C = (/) -> ( (/) ^o C ) = 1o )
8 4 7 oveqan12d 
 |-  ( ( B = (/) /\ C = (/) ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = ( ( (/) ^o (/) ) .o 1o ) )
9 0elon 
 |-  (/) e. On
10 oecl 
 |-  ( ( (/) e. On /\ (/) e. On ) -> ( (/) ^o (/) ) e. On )
11 9 9 10 mp2an 
 |-  ( (/) ^o (/) ) e. On
12 om1 
 |-  ( ( (/) ^o (/) ) e. On -> ( ( (/) ^o (/) ) .o 1o ) = ( (/) ^o (/) ) )
13 11 12 ax-mp 
 |-  ( ( (/) ^o (/) ) .o 1o ) = ( (/) ^o (/) )
14 8 13 eqtrdi 
 |-  ( ( B = (/) /\ C = (/) ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = ( (/) ^o (/) ) )
15 14 adantl 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( B = (/) /\ C = (/) ) ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = ( (/) ^o (/) ) )
16 3 15 eqtr4d 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( B = (/) /\ C = (/) ) ) -> ( (/) ^o ( B +o C ) ) = ( ( (/) ^o B ) .o ( (/) ^o C ) ) )
17 oacl 
 |-  ( ( B e. On /\ C e. On ) -> ( B +o C ) e. On )
18 on0eln0 
 |-  ( ( B +o C ) e. On -> ( (/) e. ( B +o C ) <-> ( B +o C ) =/= (/) ) )
19 17 18 syl 
 |-  ( ( B e. On /\ C e. On ) -> ( (/) e. ( B +o C ) <-> ( B +o C ) =/= (/) ) )
20 oe0m1 
 |-  ( ( B +o C ) e. On -> ( (/) e. ( B +o C ) <-> ( (/) ^o ( B +o C ) ) = (/) ) )
21 17 20 syl 
 |-  ( ( B e. On /\ C e. On ) -> ( (/) e. ( B +o C ) <-> ( (/) ^o ( B +o C ) ) = (/) ) )
22 1 necon3abid 
 |-  ( ( B e. On /\ C e. On ) -> ( ( B +o C ) =/= (/) <-> -. ( B = (/) /\ C = (/) ) ) )
23 19 21 22 3bitr3d 
 |-  ( ( B e. On /\ C e. On ) -> ( ( (/) ^o ( B +o C ) ) = (/) <-> -. ( B = (/) /\ C = (/) ) ) )
24 23 biimpar 
 |-  ( ( ( B e. On /\ C e. On ) /\ -. ( B = (/) /\ C = (/) ) ) -> ( (/) ^o ( B +o C ) ) = (/) )
25 on0eln0 
 |-  ( B e. On -> ( (/) e. B <-> B =/= (/) ) )
26 25 adantr 
 |-  ( ( B e. On /\ C e. On ) -> ( (/) e. B <-> B =/= (/) ) )
27 on0eln0 
 |-  ( C e. On -> ( (/) e. C <-> C =/= (/) ) )
28 27 adantl 
 |-  ( ( B e. On /\ C e. On ) -> ( (/) e. C <-> C =/= (/) ) )
29 26 28 orbi12d 
 |-  ( ( B e. On /\ C e. On ) -> ( ( (/) e. B \/ (/) e. C ) <-> ( B =/= (/) \/ C =/= (/) ) ) )
30 neorian 
 |-  ( ( B =/= (/) \/ C =/= (/) ) <-> -. ( B = (/) /\ C = (/) ) )
31 29 30 bitrdi 
 |-  ( ( B e. On /\ C e. On ) -> ( ( (/) e. B \/ (/) e. C ) <-> -. ( B = (/) /\ C = (/) ) ) )
32 oe0m1 
 |-  ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
33 32 biimpa 
 |-  ( ( B e. On /\ (/) e. B ) -> ( (/) ^o B ) = (/) )
34 33 oveq1d 
 |-  ( ( B e. On /\ (/) e. B ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = ( (/) .o ( (/) ^o C ) ) )
35 oecl 
 |-  ( ( (/) e. On /\ C e. On ) -> ( (/) ^o C ) e. On )
36 9 35 mpan 
 |-  ( C e. On -> ( (/) ^o C ) e. On )
37 om0r 
 |-  ( ( (/) ^o C ) e. On -> ( (/) .o ( (/) ^o C ) ) = (/) )
38 36 37 syl 
 |-  ( C e. On -> ( (/) .o ( (/) ^o C ) ) = (/) )
39 34 38 sylan9eq 
 |-  ( ( ( B e. On /\ (/) e. B ) /\ C e. On ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = (/) )
40 39 an32s 
 |-  ( ( ( B e. On /\ C e. On ) /\ (/) e. B ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = (/) )
41 oe0m1 
 |-  ( C e. On -> ( (/) e. C <-> ( (/) ^o C ) = (/) ) )
42 41 biimpa 
 |-  ( ( C e. On /\ (/) e. C ) -> ( (/) ^o C ) = (/) )
43 42 oveq2d 
 |-  ( ( C e. On /\ (/) e. C ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = ( ( (/) ^o B ) .o (/) ) )
44 oecl 
 |-  ( ( (/) e. On /\ B e. On ) -> ( (/) ^o B ) e. On )
45 9 44 mpan 
 |-  ( B e. On -> ( (/) ^o B ) e. On )
46 om0 
 |-  ( ( (/) ^o B ) e. On -> ( ( (/) ^o B ) .o (/) ) = (/) )
47 45 46 syl 
 |-  ( B e. On -> ( ( (/) ^o B ) .o (/) ) = (/) )
48 43 47 sylan9eqr 
 |-  ( ( B e. On /\ ( C e. On /\ (/) e. C ) ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = (/) )
49 48 anassrs 
 |-  ( ( ( B e. On /\ C e. On ) /\ (/) e. C ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = (/) )
50 40 49 jaodan 
 |-  ( ( ( B e. On /\ C e. On ) /\ ( (/) e. B \/ (/) e. C ) ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = (/) )
51 50 ex 
 |-  ( ( B e. On /\ C e. On ) -> ( ( (/) e. B \/ (/) e. C ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = (/) ) )
52 31 51 sylbird 
 |-  ( ( B e. On /\ C e. On ) -> ( -. ( B = (/) /\ C = (/) ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = (/) ) )
53 52 imp 
 |-  ( ( ( B e. On /\ C e. On ) /\ -. ( B = (/) /\ C = (/) ) ) -> ( ( (/) ^o B ) .o ( (/) ^o C ) ) = (/) )
54 24 53 eqtr4d 
 |-  ( ( ( B e. On /\ C e. On ) /\ -. ( B = (/) /\ C = (/) ) ) -> ( (/) ^o ( B +o C ) ) = ( ( (/) ^o B ) .o ( (/) ^o C ) ) )
55 16 54 pm2.61dan 
 |-  ( ( B e. On /\ C e. On ) -> ( (/) ^o ( B +o C ) ) = ( ( (/) ^o B ) .o ( (/) ^o C ) ) )
56 oveq1 
 |-  ( A = (/) -> ( A ^o ( B +o C ) ) = ( (/) ^o ( B +o C ) ) )
57 oveq1 
 |-  ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
58 oveq1 
 |-  ( A = (/) -> ( A ^o C ) = ( (/) ^o C ) )
59 57 58 oveq12d 
 |-  ( A = (/) -> ( ( A ^o B ) .o ( A ^o C ) ) = ( ( (/) ^o B ) .o ( (/) ^o C ) ) )
60 56 59 eqeq12d 
 |-  ( A = (/) -> ( ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) <-> ( (/) ^o ( B +o C ) ) = ( ( (/) ^o B ) .o ( (/) ^o C ) ) ) )
61 55 60 imbitrrid 
 |-  ( A = (/) -> ( ( B e. On /\ C e. On ) -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) ) )
62 61 impcom 
 |-  ( ( ( B e. On /\ C e. On ) /\ A = (/) ) -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )
63 oveq1 
 |-  ( A = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( A ^o ( B +o C ) ) = ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o ( B +o C ) ) )
64 oveq1 
 |-  ( A = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( A ^o B ) = ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o B ) )
65 oveq1 
 |-  ( A = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( A ^o C ) = ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o C ) )
66 64 65 oveq12d 
 |-  ( A = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( ( A ^o B ) .o ( A ^o C ) ) = ( ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o B ) .o ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o C ) ) )
67 63 66 eqeq12d 
 |-  ( A = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) <-> ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o ( B +o C ) ) = ( ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o B ) .o ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o C ) ) ) )
68 67 imbi2d 
 |-  ( A = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( ( C e. On -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) ) <-> ( C e. On -> ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o ( B +o C ) ) = ( ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o B ) .o ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o C ) ) ) ) )
69 oveq1 
 |-  ( B = if ( B e. On , B , 1o ) -> ( B +o C ) = ( if ( B e. On , B , 1o ) +o C ) )
70 69 oveq2d 
 |-  ( B = if ( B e. On , B , 1o ) -> ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o ( B +o C ) ) = ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o ( if ( B e. On , B , 1o ) +o C ) ) )
71 oveq2 
 |-  ( B = if ( B e. On , B , 1o ) -> ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o B ) = ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o if ( B e. On , B , 1o ) ) )
72 71 oveq1d 
 |-  ( B = if ( B e. On , B , 1o ) -> ( ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o B ) .o ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o C ) ) = ( ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o if ( B e. On , B , 1o ) ) .o ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o C ) ) )
73 70 72 eqeq12d 
 |-  ( B = if ( B e. On , B , 1o ) -> ( ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o ( B +o C ) ) = ( ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o B ) .o ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o C ) ) <-> ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o ( if ( B e. On , B , 1o ) +o C ) ) = ( ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o if ( B e. On , B , 1o ) ) .o ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o C ) ) ) )
74 73 imbi2d 
 |-  ( B = if ( B e. On , B , 1o ) -> ( ( C e. On -> ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o ( B +o C ) ) = ( ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o B ) .o ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o C ) ) ) <-> ( C e. On -> ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o ( if ( B e. On , B , 1o ) +o C ) ) = ( ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o if ( B e. On , B , 1o ) ) .o ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o C ) ) ) ) )
75 eleq1 
 |-  ( A = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( A e. On <-> if ( ( A e. On /\ (/) e. A ) , A , 1o ) e. On ) )
76 eleq2 
 |-  ( A = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( (/) e. A <-> (/) e. if ( ( A e. On /\ (/) e. A ) , A , 1o ) ) )
77 75 76 anbi12d 
 |-  ( A = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( ( A e. On /\ (/) e. A ) <-> ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) e. On /\ (/) e. if ( ( A e. On /\ (/) e. A ) , A , 1o ) ) ) )
78 eleq1 
 |-  ( 1o = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( 1o e. On <-> if ( ( A e. On /\ (/) e. A ) , A , 1o ) e. On ) )
79 eleq2 
 |-  ( 1o = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( (/) e. 1o <-> (/) e. if ( ( A e. On /\ (/) e. A ) , A , 1o ) ) )
80 78 79 anbi12d 
 |-  ( 1o = if ( ( A e. On /\ (/) e. A ) , A , 1o ) -> ( ( 1o e. On /\ (/) e. 1o ) <-> ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) e. On /\ (/) e. if ( ( A e. On /\ (/) e. A ) , A , 1o ) ) ) )
81 1on 
 |-  1o e. On
82 0lt1o 
 |-  (/) e. 1o
83 81 82 pm3.2i 
 |-  ( 1o e. On /\ (/) e. 1o )
84 77 80 83 elimhyp 
 |-  ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) e. On /\ (/) e. if ( ( A e. On /\ (/) e. A ) , A , 1o ) )
85 84 simpli 
 |-  if ( ( A e. On /\ (/) e. A ) , A , 1o ) e. On
86 84 simpri 
 |-  (/) e. if ( ( A e. On /\ (/) e. A ) , A , 1o )
87 81 elimel 
 |-  if ( B e. On , B , 1o ) e. On
88 85 86 87 oeoalem 
 |-  ( C e. On -> ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o ( if ( B e. On , B , 1o ) +o C ) ) = ( ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o if ( B e. On , B , 1o ) ) .o ( if ( ( A e. On /\ (/) e. A ) , A , 1o ) ^o C ) ) )
89 68 74 88 dedth2h 
 |-  ( ( ( A e. On /\ (/) e. A ) /\ B e. On ) -> ( C e. On -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) ) )
90 89 impr 
 |-  ( ( ( A e. On /\ (/) e. A ) /\ ( B e. On /\ C e. On ) ) -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )
91 90 an32s 
 |-  ( ( ( A e. On /\ ( B e. On /\ C e. On ) ) /\ (/) e. A ) -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )
92 62 91 oe0lem 
 |-  ( ( A e. On /\ ( B e. On /\ C e. On ) ) -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )
93 92 3impb 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )