Metamath Proof Explorer

Theorem oeoalem

Description: Lemma for oeoa . (Contributed by Eric Schmidt, 26-May-2009)

Ref Expression
Hypotheses oeoalem.1 
|- A e. On
oeoalem.2 
|- (/) e. A
oeoalem.3 
|- B e. On
Assertion oeoalem 
|- ( C e. On -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )

Proof

Step Hyp Ref Expression
1 oeoalem.1 
 |-  A e. On
2 oeoalem.2 
 |-  (/) e. A
3 oeoalem.3 
 |-  B e. On
4 oveq2 
 |-  ( x = (/) -> ( B +o x ) = ( B +o (/) ) )
5 4 oveq2d 
 |-  ( x = (/) -> ( A ^o ( B +o x ) ) = ( A ^o ( B +o (/) ) ) )
6 oveq2 
 |-  ( x = (/) -> ( A ^o x ) = ( A ^o (/) ) )
7 6 oveq2d 
 |-  ( x = (/) -> ( ( A ^o B ) .o ( A ^o x ) ) = ( ( A ^o B ) .o ( A ^o (/) ) ) )
8 5 7 eqeq12d 
 |-  ( x = (/) -> ( ( A ^o ( B +o x ) ) = ( ( A ^o B ) .o ( A ^o x ) ) <-> ( A ^o ( B +o (/) ) ) = ( ( A ^o B ) .o ( A ^o (/) ) ) ) )
9 oveq2 
 |-  ( x = y -> ( B +o x ) = ( B +o y ) )
10 9 oveq2d 
 |-  ( x = y -> ( A ^o ( B +o x ) ) = ( A ^o ( B +o y ) ) )
11 oveq2 
 |-  ( x = y -> ( A ^o x ) = ( A ^o y ) )
12 11 oveq2d 
 |-  ( x = y -> ( ( A ^o B ) .o ( A ^o x ) ) = ( ( A ^o B ) .o ( A ^o y ) ) )
13 10 12 eqeq12d 
 |-  ( x = y -> ( ( A ^o ( B +o x ) ) = ( ( A ^o B ) .o ( A ^o x ) ) <-> ( A ^o ( B +o y ) ) = ( ( A ^o B ) .o ( A ^o y ) ) ) )
14 oveq2 
 |-  ( x = suc y -> ( B +o x ) = ( B +o suc y ) )
15 14 oveq2d 
 |-  ( x = suc y -> ( A ^o ( B +o x ) ) = ( A ^o ( B +o suc y ) ) )
16 oveq2 
 |-  ( x = suc y -> ( A ^o x ) = ( A ^o suc y ) )
17 16 oveq2d 
 |-  ( x = suc y -> ( ( A ^o B ) .o ( A ^o x ) ) = ( ( A ^o B ) .o ( A ^o suc y ) ) )
18 15 17 eqeq12d 
 |-  ( x = suc y -> ( ( A ^o ( B +o x ) ) = ( ( A ^o B ) .o ( A ^o x ) ) <-> ( A ^o ( B +o suc y ) ) = ( ( A ^o B ) .o ( A ^o suc y ) ) ) )
19 oveq2 
 |-  ( x = C -> ( B +o x ) = ( B +o C ) )
20 19 oveq2d 
 |-  ( x = C -> ( A ^o ( B +o x ) ) = ( A ^o ( B +o C ) ) )
21 oveq2 
 |-  ( x = C -> ( A ^o x ) = ( A ^o C ) )
22 21 oveq2d 
 |-  ( x = C -> ( ( A ^o B ) .o ( A ^o x ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )
23 20 22 eqeq12d 
 |-  ( x = C -> ( ( A ^o ( B +o x ) ) = ( ( A ^o B ) .o ( A ^o x ) ) <-> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) ) )
24 oecl 
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
25 1 3 24 mp2an 
 |-  ( A ^o B ) e. On
26 om1 
 |-  ( ( A ^o B ) e. On -> ( ( A ^o B ) .o 1o ) = ( A ^o B ) )
27 25 26 ax-mp 
 |-  ( ( A ^o B ) .o 1o ) = ( A ^o B )
28 oe0 
 |-  ( A e. On -> ( A ^o (/) ) = 1o )
29 1 28 ax-mp 
 |-  ( A ^o (/) ) = 1o
30 29 oveq2i 
 |-  ( ( A ^o B ) .o ( A ^o (/) ) ) = ( ( A ^o B ) .o 1o )
31 oa0 
 |-  ( B e. On -> ( B +o (/) ) = B )
32 3 31 ax-mp 
 |-  ( B +o (/) ) = B
33 32 oveq2i 
 |-  ( A ^o ( B +o (/) ) ) = ( A ^o B )
34 27 30 33 3eqtr4ri 
 |-  ( A ^o ( B +o (/) ) ) = ( ( A ^o B ) .o ( A ^o (/) ) )
35 oasuc 
 |-  ( ( B e. On /\ y e. On ) -> ( B +o suc y ) = suc ( B +o y ) )
36 35 oveq2d 
 |-  ( ( B e. On /\ y e. On ) -> ( A ^o ( B +o suc y ) ) = ( A ^o suc ( B +o y ) ) )
37 oacl 
 |-  ( ( B e. On /\ y e. On ) -> ( B +o y ) e. On )
38 oesuc 
 |-  ( ( A e. On /\ ( B +o y ) e. On ) -> ( A ^o suc ( B +o y ) ) = ( ( A ^o ( B +o y ) ) .o A ) )
39 1 37 38 sylancr 
 |-  ( ( B e. On /\ y e. On ) -> ( A ^o suc ( B +o y ) ) = ( ( A ^o ( B +o y ) ) .o A ) )
40 36 39 eqtrd 
 |-  ( ( B e. On /\ y e. On ) -> ( A ^o ( B +o suc y ) ) = ( ( A ^o ( B +o y ) ) .o A ) )
41 3 40 mpan 
 |-  ( y e. On -> ( A ^o ( B +o suc y ) ) = ( ( A ^o ( B +o y ) ) .o A ) )
42 oveq1 
 |-  ( ( A ^o ( B +o y ) ) = ( ( A ^o B ) .o ( A ^o y ) ) -> ( ( A ^o ( B +o y ) ) .o A ) = ( ( ( A ^o B ) .o ( A ^o y ) ) .o A ) )
43 41 42 sylan9eq 
 |-  ( ( y e. On /\ ( A ^o ( B +o y ) ) = ( ( A ^o B ) .o ( A ^o y ) ) ) -> ( A ^o ( B +o suc y ) ) = ( ( ( A ^o B ) .o ( A ^o y ) ) .o A ) )
44 oecl 
 |-  ( ( A e. On /\ y e. On ) -> ( A ^o y ) e. On )
45 omass 
 |-  ( ( ( A ^o B ) e. On /\ ( A ^o y ) e. On /\ A e. On ) -> ( ( ( A ^o B ) .o ( A ^o y ) ) .o A ) = ( ( A ^o B ) .o ( ( A ^o y ) .o A ) ) )
46 25 1 45 mp3an13 
 |-  ( ( A ^o y ) e. On -> ( ( ( A ^o B ) .o ( A ^o y ) ) .o A ) = ( ( A ^o B ) .o ( ( A ^o y ) .o A ) ) )
47 44 46 syl 
 |-  ( ( A e. On /\ y e. On ) -> ( ( ( A ^o B ) .o ( A ^o y ) ) .o A ) = ( ( A ^o B ) .o ( ( A ^o y ) .o A ) ) )
48 oesuc 
 |-  ( ( A e. On /\ y e. On ) -> ( A ^o suc y ) = ( ( A ^o y ) .o A ) )
49 48 oveq2d 
 |-  ( ( A e. On /\ y e. On ) -> ( ( A ^o B ) .o ( A ^o suc y ) ) = ( ( A ^o B ) .o ( ( A ^o y ) .o A ) ) )
50 47 49 eqtr4d 
 |-  ( ( A e. On /\ y e. On ) -> ( ( ( A ^o B ) .o ( A ^o y ) ) .o A ) = ( ( A ^o B ) .o ( A ^o suc y ) ) )
51 1 50 mpan 
 |-  ( y e. On -> ( ( ( A ^o B ) .o ( A ^o y ) ) .o A ) = ( ( A ^o B ) .o ( A ^o suc y ) ) )
52 51 adantr 
 |-  ( ( y e. On /\ ( A ^o ( B +o y ) ) = ( ( A ^o B ) .o ( A ^o y ) ) ) -> ( ( ( A ^o B ) .o ( A ^o y ) ) .o A ) = ( ( A ^o B ) .o ( A ^o suc y ) ) )
53 43 52 eqtrd 
 |-  ( ( y e. On /\ ( A ^o ( B +o y ) ) = ( ( A ^o B ) .o ( A ^o y ) ) ) -> ( A ^o ( B +o suc y ) ) = ( ( A ^o B ) .o ( A ^o suc y ) ) )
54 53 ex 
 |-  ( y e. On -> ( ( A ^o ( B +o y ) ) = ( ( A ^o B ) .o ( A ^o y ) ) -> ( A ^o ( B +o suc y ) ) = ( ( A ^o B ) .o ( A ^o suc y ) ) ) )
55 vex 
 |-  x e. _V
56 oalim 
 |-  ( ( B e. On /\ ( x e. _V /\ Lim x ) ) -> ( B +o x ) = U_ y e. x ( B +o y ) )
57 3 56 mpan 
 |-  ( ( x e. _V /\ Lim x ) -> ( B +o x ) = U_ y e. x ( B +o y ) )
58 55 57 mpan 
 |-  ( Lim x -> ( B +o x ) = U_ y e. x ( B +o y ) )
59 58 oveq2d 
 |-  ( Lim x -> ( A ^o ( B +o x ) ) = ( A ^o U_ y e. x ( B +o y ) ) )
60 limord 
 |-  ( Lim x -> Ord x )
61 ordelon 
 |-  ( ( Ord x /\ y e. x ) -> y e. On )
62 60 61 sylan 
 |-  ( ( Lim x /\ y e. x ) -> y e. On )
63 3 62 37 sylancr 
 |-  ( ( Lim x /\ y e. x ) -> ( B +o y ) e. On )
64 63 ralrimiva 
 |-  ( Lim x -> A. y e. x ( B +o y ) e. On )
65 0ellim 
 |-  ( Lim x -> (/) e. x )
66 65 ne0d 
 |-  ( Lim x -> x =/= (/) )
67 vex 
 |-  w e. _V
68 oelim 
 |-  ( ( ( A e. On /\ ( w e. _V /\ Lim w ) ) /\ (/) e. A ) -> ( A ^o w ) = U_ z e. w ( A ^o z ) )
69 2 68 mpan2 
 |-  ( ( A e. On /\ ( w e. _V /\ Lim w ) ) -> ( A ^o w ) = U_ z e. w ( A ^o z ) )
70 1 69 mpan 
 |-  ( ( w e. _V /\ Lim w ) -> ( A ^o w ) = U_ z e. w ( A ^o z ) )
71 67 70 mpan 
 |-  ( Lim w -> ( A ^o w ) = U_ z e. w ( A ^o z ) )
72 oewordi 
 |-  ( ( ( z e. On /\ w e. On /\ A e. On ) /\ (/) e. A ) -> ( z C_ w -> ( A ^o z ) C_ ( A ^o w ) ) )
73 2 72 mpan2 
 |-  ( ( z e. On /\ w e. On /\ A e. On ) -> ( z C_ w -> ( A ^o z ) C_ ( A ^o w ) ) )
74 1 73 mp3an3 
 |-  ( ( z e. On /\ w e. On ) -> ( z C_ w -> ( A ^o z ) C_ ( A ^o w ) ) )
75 74 3impia 
 |-  ( ( z e. On /\ w e. On /\ z C_ w ) -> ( A ^o z ) C_ ( A ^o w ) )
76 71 75 onoviun 
 |-  ( ( x e. _V /\ A. y e. x ( B +o y ) e. On /\ x =/= (/) ) -> ( A ^o U_ y e. x ( B +o y ) ) = U_ y e. x ( A ^o ( B +o y ) ) )
77 55 64 66 76 mp3an2i 
 |-  ( Lim x -> ( A ^o U_ y e. x ( B +o y ) ) = U_ y e. x ( A ^o ( B +o y ) ) )
78 59 77 eqtrd 
 |-  ( Lim x -> ( A ^o ( B +o x ) ) = U_ y e. x ( A ^o ( B +o y ) ) )
79 iuneq2 
 |-  ( A. y e. x ( A ^o ( B +o y ) ) = ( ( A ^o B ) .o ( A ^o y ) ) -> U_ y e. x ( A ^o ( B +o y ) ) = U_ y e. x ( ( A ^o B ) .o ( A ^o y ) ) )
80 78 79 sylan9eq 
 |-  ( ( Lim x /\ A. y e. x ( A ^o ( B +o y ) ) = ( ( A ^o B ) .o ( A ^o y ) ) ) -> ( A ^o ( B +o x ) ) = U_ y e. x ( ( A ^o B ) .o ( A ^o y ) ) )
81 oelim 
 |-  ( ( ( A e. On /\ ( x e. _V /\ Lim x ) ) /\ (/) e. A ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
82 2 81 mpan2 
 |-  ( ( A e. On /\ ( x e. _V /\ Lim x ) ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
83 1 82 mpan 
 |-  ( ( x e. _V /\ Lim x ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
84 55 83 mpan 
 |-  ( Lim x -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
85 84 oveq2d 
 |-  ( Lim x -> ( ( A ^o B ) .o ( A ^o x ) ) = ( ( A ^o B ) .o U_ y e. x ( A ^o y ) ) )
86 1 62 44 sylancr 
 |-  ( ( Lim x /\ y e. x ) -> ( A ^o y ) e. On )
87 86 ralrimiva 
 |-  ( Lim x -> A. y e. x ( A ^o y ) e. On )
88 omlim 
 |-  ( ( ( A ^o B ) e. On /\ ( w e. _V /\ Lim w ) ) -> ( ( A ^o B ) .o w ) = U_ z e. w ( ( A ^o B ) .o z ) )
89 25 88 mpan 
 |-  ( ( w e. _V /\ Lim w ) -> ( ( A ^o B ) .o w ) = U_ z e. w ( ( A ^o B ) .o z ) )
90 67 89 mpan 
 |-  ( Lim w -> ( ( A ^o B ) .o w ) = U_ z e. w ( ( A ^o B ) .o z ) )
91 omwordi 
 |-  ( ( z e. On /\ w e. On /\ ( A ^o B ) e. On ) -> ( z C_ w -> ( ( A ^o B ) .o z ) C_ ( ( A ^o B ) .o w ) ) )
92 25 91 mp3an3 
 |-  ( ( z e. On /\ w e. On ) -> ( z C_ w -> ( ( A ^o B ) .o z ) C_ ( ( A ^o B ) .o w ) ) )
93 92 3impia 
 |-  ( ( z e. On /\ w e. On /\ z C_ w ) -> ( ( A ^o B ) .o z ) C_ ( ( A ^o B ) .o w ) )
94 90 93 onoviun 
 |-  ( ( x e. _V /\ A. y e. x ( A ^o y ) e. On /\ x =/= (/) ) -> ( ( A ^o B ) .o U_ y e. x ( A ^o y ) ) = U_ y e. x ( ( A ^o B ) .o ( A ^o y ) ) )
95 55 87 66 94 mp3an2i 
 |-  ( Lim x -> ( ( A ^o B ) .o U_ y e. x ( A ^o y ) ) = U_ y e. x ( ( A ^o B ) .o ( A ^o y ) ) )
96 85 95 eqtrd 
 |-  ( Lim x -> ( ( A ^o B ) .o ( A ^o x ) ) = U_ y e. x ( ( A ^o B ) .o ( A ^o y ) ) )
97 96 adantr 
 |-  ( ( Lim x /\ A. y e. x ( A ^o ( B +o y ) ) = ( ( A ^o B ) .o ( A ^o y ) ) ) -> ( ( A ^o B ) .o ( A ^o x ) ) = U_ y e. x ( ( A ^o B ) .o ( A ^o y ) ) )
98 80 97 eqtr4d 
 |-  ( ( Lim x /\ A. y e. x ( A ^o ( B +o y ) ) = ( ( A ^o B ) .o ( A ^o y ) ) ) -> ( A ^o ( B +o x ) ) = ( ( A ^o B ) .o ( A ^o x ) ) )
99 98 ex 
 |-  ( Lim x -> ( A. y e. x ( A ^o ( B +o y ) ) = ( ( A ^o B ) .o ( A ^o y ) ) -> ( A ^o ( B +o x ) ) = ( ( A ^o B ) .o ( A ^o x ) ) ) )
100 8 13 18 23 34 54 99 tfinds 
 |-  ( C e. On -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )