This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem omass

Description: Multiplication of ordinal numbers is associative. Theorem 8.26 of TakeutiZaring p. 65. Theorem 4.4 of Schloeder p. 13. (Contributed by NM, 28-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = (/) -> ( ( A .o B ) .o x ) = ( ( A .o B ) .o (/) ) )
2 oveq2 
 |-  ( x = (/) -> ( B .o x ) = ( B .o (/) ) )
3 2 oveq2d 
 |-  ( x = (/) -> ( A .o ( B .o x ) ) = ( A .o ( B .o (/) ) ) )
4 1 3 eqeq12d 
 |-  ( x = (/) -> ( ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) <-> ( ( A .o B ) .o (/) ) = ( A .o ( B .o (/) ) ) ) )
5 oveq2 
 |-  ( x = y -> ( ( A .o B ) .o x ) = ( ( A .o B ) .o y ) )
6 oveq2 
 |-  ( x = y -> ( B .o x ) = ( B .o y ) )
7 6 oveq2d 
 |-  ( x = y -> ( A .o ( B .o x ) ) = ( A .o ( B .o y ) ) )
8 5 7 eqeq12d 
 |-  ( x = y -> ( ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) <-> ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) ) )
9 oveq2 
 |-  ( x = suc y -> ( ( A .o B ) .o x ) = ( ( A .o B ) .o suc y ) )
10 oveq2 
 |-  ( x = suc y -> ( B .o x ) = ( B .o suc y ) )
11 10 oveq2d 
 |-  ( x = suc y -> ( A .o ( B .o x ) ) = ( A .o ( B .o suc y ) ) )
12 9 11 eqeq12d 
 |-  ( x = suc y -> ( ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) <-> ( ( A .o B ) .o suc y ) = ( A .o ( B .o suc y ) ) ) )
13 oveq2 
 |-  ( x = C -> ( ( A .o B ) .o x ) = ( ( A .o B ) .o C ) )
14 oveq2 
 |-  ( x = C -> ( B .o x ) = ( B .o C ) )
15 14 oveq2d 
 |-  ( x = C -> ( A .o ( B .o x ) ) = ( A .o ( B .o C ) ) )
16 13 15 eqeq12d 
 |-  ( x = C -> ( ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) <-> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) ) )
17 omcl 
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
18 om0 
 |-  ( ( A .o B ) e. On -> ( ( A .o B ) .o (/) ) = (/) )
19 17 18 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o B ) .o (/) ) = (/) )
20 om0 
 |-  ( B e. On -> ( B .o (/) ) = (/) )
21 20 oveq2d 
 |-  ( B e. On -> ( A .o ( B .o (/) ) ) = ( A .o (/) ) )
22 om0 
 |-  ( A e. On -> ( A .o (/) ) = (/) )
23 21 22 sylan9eqr 
 |-  ( ( A e. On /\ B e. On ) -> ( A .o ( B .o (/) ) ) = (/) )
24 19 23 eqtr4d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o B ) .o (/) ) = ( A .o ( B .o (/) ) ) )
25 oveq1 
 |-  ( ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( ( A .o B ) .o y ) +o ( A .o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) )
26 omsuc 
 |-  ( ( ( A .o B ) e. On /\ y e. On ) -> ( ( A .o B ) .o suc y ) = ( ( ( A .o B ) .o y ) +o ( A .o B ) ) )
27 17 26 stoic3 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( ( A .o B ) .o suc y ) = ( ( ( A .o B ) .o y ) +o ( A .o B ) ) )
28 omsuc 
 |-  ( ( B e. On /\ y e. On ) -> ( B .o suc y ) = ( ( B .o y ) +o B ) )
29 28 3adant1 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( B .o suc y ) = ( ( B .o y ) +o B ) )
30 29 oveq2d 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( A .o ( B .o suc y ) ) = ( A .o ( ( B .o y ) +o B ) ) )
31 omcl 
 |-  ( ( B e. On /\ y e. On ) -> ( B .o y ) e. On )
32 odi 
 |-  ( ( A e. On /\ ( B .o y ) e. On /\ B e. On ) -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) )
33 31 32 syl3an2 
 |-  ( ( A e. On /\ ( B e. On /\ y e. On ) /\ B e. On ) -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) )
34 33 3exp 
 |-  ( A e. On -> ( ( B e. On /\ y e. On ) -> ( B e. On -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) ) ) )
35 34 expd 
 |-  ( A e. On -> ( B e. On -> ( y e. On -> ( B e. On -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) ) ) ) )
36 35 com34 
 |-  ( A e. On -> ( B e. On -> ( B e. On -> ( y e. On -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) ) ) ) )
37 36 pm2.43d 
 |-  ( A e. On -> ( B e. On -> ( y e. On -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) ) ) )
38 37 3imp 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) )
39 30 38 eqtrd 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( A .o ( B .o suc y ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) )
40 27 39 eqeq12d 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( ( ( A .o B ) .o suc y ) = ( A .o ( B .o suc y ) ) <-> ( ( ( A .o B ) .o y ) +o ( A .o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) ) )
41 25 40 imbitrrid 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o suc y ) = ( A .o ( B .o suc y ) ) ) )
42 41 3exp 
 |-  ( A e. On -> ( B e. On -> ( y e. On -> ( ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o suc y ) = ( A .o ( B .o suc y ) ) ) ) ) )
43 42 com3r 
 |-  ( y e. On -> ( A e. On -> ( B e. On -> ( ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o suc y ) = ( A .o ( B .o suc y ) ) ) ) ) )
44 43 impd 
 |-  ( y e. On -> ( ( A e. On /\ B e. On ) -> ( ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o suc y ) = ( A .o ( B .o suc y ) ) ) ) )
45 17 ancoms 
 |-  ( ( B e. On /\ A e. On ) -> ( A .o B ) e. On )
46 vex 
 |-  x e. _V
47 omlim 
 |-  ( ( ( A .o B ) e. On /\ ( x e. _V /\ Lim x ) ) -> ( ( A .o B ) .o x ) = U_ y e. x ( ( A .o B ) .o y ) )
48 46 47 mpanr1 
 |-  ( ( ( A .o B ) e. On /\ Lim x ) -> ( ( A .o B ) .o x ) = U_ y e. x ( ( A .o B ) .o y ) )
49 45 48 sylan 
 |-  ( ( ( B e. On /\ A e. On ) /\ Lim x ) -> ( ( A .o B ) .o x ) = U_ y e. x ( ( A .o B ) .o y ) )
50 49 an32s 
 |-  ( ( ( B e. On /\ Lim x ) /\ A e. On ) -> ( ( A .o B ) .o x ) = U_ y e. x ( ( A .o B ) .o y ) )
51 50 ad2antrr 
 |-  ( ( ( ( ( B e. On /\ Lim x ) /\ A e. On ) /\ (/) e. B ) /\ A. y e. x ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) ) -> ( ( A .o B ) .o x ) = U_ y e. x ( ( A .o B ) .o y ) )
52 iuneq2 
 |-  ( A. y e. x ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> U_ y e. x ( ( A .o B ) .o y ) = U_ y e. x ( A .o ( B .o y ) ) )
53 limelon 
 |-  ( ( x e. _V /\ Lim x ) -> x e. On )
54 46 53 mpan 
 |-  ( Lim x -> x e. On )
55 54 anim1i 
 |-  ( ( Lim x /\ B e. On ) -> ( x e. On /\ B e. On ) )
56 55 ancoms 
 |-  ( ( B e. On /\ Lim x ) -> ( x e. On /\ B e. On ) )
57 omordi 
 |-  ( ( ( x e. On /\ B e. On ) /\ (/) e. B ) -> ( y e. x -> ( B .o y ) e. ( B .o x ) ) )
58 56 57 sylan 
 |-  ( ( ( B e. On /\ Lim x ) /\ (/) e. B ) -> ( y e. x -> ( B .o y ) e. ( B .o x ) ) )
59 ssid 
 |-  ( A .o ( B .o y ) ) C_ ( A .o ( B .o y ) )
60 oveq2 
 |-  ( z = ( B .o y ) -> ( A .o z ) = ( A .o ( B .o y ) ) )
61 60 sseq2d 
 |-  ( z = ( B .o y ) -> ( ( A .o ( B .o y ) ) C_ ( A .o z ) <-> ( A .o ( B .o y ) ) C_ ( A .o ( B .o y ) ) ) )
62 61 rspcev 
 |-  ( ( ( B .o y ) e. ( B .o x ) /\ ( A .o ( B .o y ) ) C_ ( A .o ( B .o y ) ) ) -> E. z e. ( B .o x ) ( A .o ( B .o y ) ) C_ ( A .o z ) )
63 59 62 mpan2 
 |-  ( ( B .o y ) e. ( B .o x ) -> E. z e. ( B .o x ) ( A .o ( B .o y ) ) C_ ( A .o z ) )
64 58 63 syl6 
 |-  ( ( ( B e. On /\ Lim x ) /\ (/) e. B ) -> ( y e. x -> E. z e. ( B .o x ) ( A .o ( B .o y ) ) C_ ( A .o z ) ) )
65 64 ralrimiv 
 |-  ( ( ( B e. On /\ Lim x ) /\ (/) e. B ) -> A. y e. x E. z e. ( B .o x ) ( A .o ( B .o y ) ) C_ ( A .o z ) )
66 iunss2 
 |-  ( A. y e. x E. z e. ( B .o x ) ( A .o ( B .o y ) ) C_ ( A .o z ) -> U_ y e. x ( A .o ( B .o y ) ) C_ U_ z e. ( B .o x ) ( A .o z ) )
67 65 66 syl 
 |-  ( ( ( B e. On /\ Lim x ) /\ (/) e. B ) -> U_ y e. x ( A .o ( B .o y ) ) C_ U_ z e. ( B .o x ) ( A .o z ) )
68 67 adantlr 
 |-  ( ( ( ( B e. On /\ Lim x ) /\ A e. On ) /\ (/) e. B ) -> U_ y e. x ( A .o ( B .o y ) ) C_ U_ z e. ( B .o x ) ( A .o z ) )
69 omcl 
 |-  ( ( B e. On /\ x e. On ) -> ( B .o x ) e. On )
70 54 69 sylan2 
 |-  ( ( B e. On /\ Lim x ) -> ( B .o x ) e. On )
71 onelon 
 |-  ( ( ( B .o x ) e. On /\ z e. ( B .o x ) ) -> z e. On )
72 70 71 sylan 
 |-  ( ( ( B e. On /\ Lim x ) /\ z e. ( B .o x ) ) -> z e. On )
73 72 adantlr 
 |-  ( ( ( ( B e. On /\ Lim x ) /\ A e. On ) /\ z e. ( B .o x ) ) -> z e. On )
74 omordlim 
 |-  ( ( ( B e. On /\ ( x e. _V /\ Lim x ) ) /\ z e. ( B .o x ) ) -> E. y e. x z e. ( B .o y ) )
75 74 ex 
 |-  ( ( B e. On /\ ( x e. _V /\ Lim x ) ) -> ( z e. ( B .o x ) -> E. y e. x z e. ( B .o y ) ) )
76 46 75 mpanr1 
 |-  ( ( B e. On /\ Lim x ) -> ( z e. ( B .o x ) -> E. y e. x z e. ( B .o y ) ) )
77 76 ad2antlr 
 |-  ( ( ( z e. On /\ ( B e. On /\ Lim x ) ) /\ A e. On ) -> ( z e. ( B .o x ) -> E. y e. x z e. ( B .o y ) ) )
78 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
79 54 78 sylan 
 |-  ( ( Lim x /\ y e. x ) -> y e. On )
80 79 31 sylan2 
 |-  ( ( B e. On /\ ( Lim x /\ y e. x ) ) -> ( B .o y ) e. On )
81 onelss 
 |-  ( ( B .o y ) e. On -> ( z e. ( B .o y ) -> z C_ ( B .o y ) ) )
82 81 3ad2ant2 
 |-  ( ( z e. On /\ ( B .o y ) e. On /\ A e. On ) -> ( z e. ( B .o y ) -> z C_ ( B .o y ) ) )
83 omwordi 
 |-  ( ( z e. On /\ ( B .o y ) e. On /\ A e. On ) -> ( z C_ ( B .o y ) -> ( A .o z ) C_ ( A .o ( B .o y ) ) ) )
84 82 83 syld 
 |-  ( ( z e. On /\ ( B .o y ) e. On /\ A e. On ) -> ( z e. ( B .o y ) -> ( A .o z ) C_ ( A .o ( B .o y ) ) ) )
85 84 3exp 
 |-  ( z e. On -> ( ( B .o y ) e. On -> ( A e. On -> ( z e. ( B .o y ) -> ( A .o z ) C_ ( A .o ( B .o y ) ) ) ) ) )
86 80 85 syl5 
 |-  ( z e. On -> ( ( B e. On /\ ( Lim x /\ y e. x ) ) -> ( A e. On -> ( z e. ( B .o y ) -> ( A .o z ) C_ ( A .o ( B .o y ) ) ) ) ) )
87 86 exp4d 
 |-  ( z e. On -> ( B e. On -> ( Lim x -> ( y e. x -> ( A e. On -> ( z e. ( B .o y ) -> ( A .o z ) C_ ( A .o ( B .o y ) ) ) ) ) ) ) )
88 87 imp32 
 |-  ( ( z e. On /\ ( B e. On /\ Lim x ) ) -> ( y e. x -> ( A e. On -> ( z e. ( B .o y ) -> ( A .o z ) C_ ( A .o ( B .o y ) ) ) ) ) )
89 88 com23 
 |-  ( ( z e. On /\ ( B e. On /\ Lim x ) ) -> ( A e. On -> ( y e. x -> ( z e. ( B .o y ) -> ( A .o z ) C_ ( A .o ( B .o y ) ) ) ) ) )
90 89 imp 
 |-  ( ( ( z e. On /\ ( B e. On /\ Lim x ) ) /\ A e. On ) -> ( y e. x -> ( z e. ( B .o y ) -> ( A .o z ) C_ ( A .o ( B .o y ) ) ) ) )
91 90 reximdvai 
 |-  ( ( ( z e. On /\ ( B e. On /\ Lim x ) ) /\ A e. On ) -> ( E. y e. x z e. ( B .o y ) -> E. y e. x ( A .o z ) C_ ( A .o ( B .o y ) ) ) )
92 77 91 syld 
 |-  ( ( ( z e. On /\ ( B e. On /\ Lim x ) ) /\ A e. On ) -> ( z e. ( B .o x ) -> E. y e. x ( A .o z ) C_ ( A .o ( B .o y ) ) ) )
93 92 exp31 
 |-  ( z e. On -> ( ( B e. On /\ Lim x ) -> ( A e. On -> ( z e. ( B .o x ) -> E. y e. x ( A .o z ) C_ ( A .o ( B .o y ) ) ) ) ) )
94 93 imp4c 
 |-  ( z e. On -> ( ( ( ( B e. On /\ Lim x ) /\ A e. On ) /\ z e. ( B .o x ) ) -> E. y e. x ( A .o z ) C_ ( A .o ( B .o y ) ) ) )
95 73 94 mpcom 
 |-  ( ( ( ( B e. On /\ Lim x ) /\ A e. On ) /\ z e. ( B .o x ) ) -> E. y e. x ( A .o z ) C_ ( A .o ( B .o y ) ) )
96 95 ralrimiva 
 |-  ( ( ( B e. On /\ Lim x ) /\ A e. On ) -> A. z e. ( B .o x ) E. y e. x ( A .o z ) C_ ( A .o ( B .o y ) ) )
97 iunss2 
 |-  ( A. z e. ( B .o x ) E. y e. x ( A .o z ) C_ ( A .o ( B .o y ) ) -> U_ z e. ( B .o x ) ( A .o z ) C_ U_ y e. x ( A .o ( B .o y ) ) )
98 96 97 syl 
 |-  ( ( ( B e. On /\ Lim x ) /\ A e. On ) -> U_ z e. ( B .o x ) ( A .o z ) C_ U_ y e. x ( A .o ( B .o y ) ) )
99 98 adantr 
 |-  ( ( ( ( B e. On /\ Lim x ) /\ A e. On ) /\ (/) e. B ) -> U_ z e. ( B .o x ) ( A .o z ) C_ U_ y e. x ( A .o ( B .o y ) ) )
100 68 99 eqssd 
 |-  ( ( ( ( B e. On /\ Lim x ) /\ A e. On ) /\ (/) e. B ) -> U_ y e. x ( A .o ( B .o y ) ) = U_ z e. ( B .o x ) ( A .o z ) )
101 omlimcl 
 |-  ( ( ( B e. On /\ ( x e. _V /\ Lim x ) ) /\ (/) e. B ) -> Lim ( B .o x ) )
102 46 101 mpanlr1 
 |-  ( ( ( B e. On /\ Lim x ) /\ (/) e. B ) -> Lim ( B .o x ) )
103 ovex 
 |-  ( B .o x ) e. _V
104 omlim 
 |-  ( ( A e. On /\ ( ( B .o x ) e. _V /\ Lim ( B .o x ) ) ) -> ( A .o ( B .o x ) ) = U_ z e. ( B .o x ) ( A .o z ) )
105 103 104 mpanr1 
 |-  ( ( A e. On /\ Lim ( B .o x ) ) -> ( A .o ( B .o x ) ) = U_ z e. ( B .o x ) ( A .o z ) )
106 102 105 sylan2 
 |-  ( ( A e. On /\ ( ( B e. On /\ Lim x ) /\ (/) e. B ) ) -> ( A .o ( B .o x ) ) = U_ z e. ( B .o x ) ( A .o z ) )
107 106 ancoms 
 |-  ( ( ( ( B e. On /\ Lim x ) /\ (/) e. B ) /\ A e. On ) -> ( A .o ( B .o x ) ) = U_ z e. ( B .o x ) ( A .o z ) )
108 107 an32s 
 |-  ( ( ( ( B e. On /\ Lim x ) /\ A e. On ) /\ (/) e. B ) -> ( A .o ( B .o x ) ) = U_ z e. ( B .o x ) ( A .o z ) )
109 100 108 eqtr4d 
 |-  ( ( ( ( B e. On /\ Lim x ) /\ A e. On ) /\ (/) e. B ) -> U_ y e. x ( A .o ( B .o y ) ) = ( A .o ( B .o x ) ) )
110 52 109 sylan9eqr 
 |-  ( ( ( ( ( B e. On /\ Lim x ) /\ A e. On ) /\ (/) e. B ) /\ A. y e. x ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) ) -> U_ y e. x ( ( A .o B ) .o y ) = ( A .o ( B .o x ) ) )
111 51 110 eqtrd 
 |-  ( ( ( ( ( B e. On /\ Lim x ) /\ A e. On ) /\ (/) e. B ) /\ A. y e. x ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) ) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) )
112 111 exp31 
 |-  ( ( ( B e. On /\ Lim x ) /\ A e. On ) -> ( (/) e. B -> ( A. y e. x ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) ) ) )
113 eloni 
 |-  ( B e. On -> Ord B )
114 ord0eln0 
 |-  ( Ord B -> ( (/) e. B <-> B =/= (/) ) )
115 114 necon2bbid 
 |-  ( Ord B -> ( B = (/) <-> -. (/) e. B ) )
116 113 115 syl 
 |-  ( B e. On -> ( B = (/) <-> -. (/) e. B ) )
117 116 ad2antrr 
 |-  ( ( ( B e. On /\ Lim x ) /\ A e. On ) -> ( B = (/) <-> -. (/) e. B ) )
118 oveq2 
 |-  ( B = (/) -> ( A .o B ) = ( A .o (/) ) )
119 118 22 sylan9eqr 
 |-  ( ( A e. On /\ B = (/) ) -> ( A .o B ) = (/) )
120 119 oveq1d 
 |-  ( ( A e. On /\ B = (/) ) -> ( ( A .o B ) .o x ) = ( (/) .o x ) )
121 om0r 
 |-  ( x e. On -> ( (/) .o x ) = (/) )
122 120 121 sylan9eqr 
 |-  ( ( x e. On /\ ( A e. On /\ B = (/) ) ) -> ( ( A .o B ) .o x ) = (/) )
123 122 anassrs 
 |-  ( ( ( x e. On /\ A e. On ) /\ B = (/) ) -> ( ( A .o B ) .o x ) = (/) )
124 oveq1 
 |-  ( B = (/) -> ( B .o x ) = ( (/) .o x ) )
125 124 121 sylan9eqr 
 |-  ( ( x e. On /\ B = (/) ) -> ( B .o x ) = (/) )
126 125 oveq2d 
 |-  ( ( x e. On /\ B = (/) ) -> ( A .o ( B .o x ) ) = ( A .o (/) ) )
127 126 22 sylan9eq 
 |-  ( ( ( x e. On /\ B = (/) ) /\ A e. On ) -> ( A .o ( B .o x ) ) = (/) )
128 127 an32s 
 |-  ( ( ( x e. On /\ A e. On ) /\ B = (/) ) -> ( A .o ( B .o x ) ) = (/) )
129 123 128 eqtr4d 
 |-  ( ( ( x e. On /\ A e. On ) /\ B = (/) ) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) )
130 129 ex 
 |-  ( ( x e. On /\ A e. On ) -> ( B = (/) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) ) )
131 54 130 sylan 
 |-  ( ( Lim x /\ A e. On ) -> ( B = (/) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) ) )
132 131 adantll 
 |-  ( ( ( B e. On /\ Lim x ) /\ A e. On ) -> ( B = (/) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) ) )
133 117 132 sylbird 
 |-  ( ( ( B e. On /\ Lim x ) /\ A e. On ) -> ( -. (/) e. B -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) ) )
134 133 a1dd 
 |-  ( ( ( B e. On /\ Lim x ) /\ A e. On ) -> ( -. (/) e. B -> ( A. y e. x ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) ) ) )
135 112 134 pm2.61d 
 |-  ( ( ( B e. On /\ Lim x ) /\ A e. On ) -> ( A. y e. x ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) ) )
136 135 exp31 
 |-  ( B e. On -> ( Lim x -> ( A e. On -> ( A. y e. x ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) ) ) ) )
137 136 com3l 
 |-  ( Lim x -> ( A e. On -> ( B e. On -> ( A. y e. x ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) ) ) ) )
138 137 impd 
 |-  ( Lim x -> ( ( A e. On /\ B e. On ) -> ( A. y e. x ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) ) ) )
139 4 8 12 16 24 44 138 tfinds3 
 |-  ( C e. On -> ( ( A e. On /\ B e. On ) -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) ) )
140 139 expd 
 |-  ( C e. On -> ( A e. On -> ( B e. On -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) ) ) )
141 140 com3l 
 |-  ( A e. On -> ( B e. On -> ( C e. On -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) ) ) )
142 141 3imp 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) )