Metamath Proof Explorer


Theorem omeu

Description: The division algorithm for ordinal multiplication. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion omeu A On B On A ∃! z x On y A z = x y A 𝑜 x + 𝑜 y = B

Proof

Step Hyp Ref Expression
1 omeulem1 A On B On A x On y A A 𝑜 x + 𝑜 y = B
2 opex x y V
3 2 isseti z z = x y
4 19.41v z z = x y A 𝑜 x + 𝑜 y = B z z = x y A 𝑜 x + 𝑜 y = B
5 3 4 mpbiran z z = x y A 𝑜 x + 𝑜 y = B A 𝑜 x + 𝑜 y = B
6 5 rexbii y A z z = x y A 𝑜 x + 𝑜 y = B y A A 𝑜 x + 𝑜 y = B
7 rexcom4 y A z z = x y A 𝑜 x + 𝑜 y = B z y A z = x y A 𝑜 x + 𝑜 y = B
8 6 7 bitr3i y A A 𝑜 x + 𝑜 y = B z y A z = x y A 𝑜 x + 𝑜 y = B
9 8 rexbii x On y A A 𝑜 x + 𝑜 y = B x On z y A z = x y A 𝑜 x + 𝑜 y = B
10 rexcom4 x On z y A z = x y A 𝑜 x + 𝑜 y = B z x On y A z = x y A 𝑜 x + 𝑜 y = B
11 9 10 bitri x On y A A 𝑜 x + 𝑜 y = B z x On y A z = x y A 𝑜 x + 𝑜 y = B
12 1 11 sylib A On B On A z x On y A z = x y A 𝑜 x + 𝑜 y = B
13 simp2rl A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B z = x y
14 simp3rl A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B t = r s
15 simp2rr A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B A 𝑜 x + 𝑜 y = B
16 simp3rr A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B A 𝑜 r + 𝑜 s = B
17 15 16 eqtr4d A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B A 𝑜 x + 𝑜 y = A 𝑜 r + 𝑜 s
18 simp11 A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B A On
19 simp13 A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B A
20 simp2ll A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B x On
21 simp2lr A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B y A
22 simp3ll A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B r On
23 simp3lr A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B s A
24 omopth2 A On A x On y A r On s A A 𝑜 x + 𝑜 y = A 𝑜 r + 𝑜 s x = r y = s
25 18 19 20 21 22 23 24 syl222anc A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B A 𝑜 x + 𝑜 y = A 𝑜 r + 𝑜 s x = r y = s
26 17 25 mpbid A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B x = r y = s
27 opeq12 x = r y = s x y = r s
28 26 27 syl A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B x y = r s
29 14 28 eqtr4d A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B t = x y
30 13 29 eqtr4d A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B z = t
31 30 3expia A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B z = t
32 31 exp4b A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B z = t
33 32 expd A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B z = t
34 33 rexlimdvv A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B z = t
35 34 imp A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B z = t
36 35 rexlimdvv A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B z = t
37 36 expimpd A On B On A x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B z = t
38 37 alrimivv A On B On A z t x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B z = t
39 opeq1 x = r x y = r y
40 39 eqeq2d x = r z = x y z = r y
41 oveq2 x = r A 𝑜 x = A 𝑜 r
42 41 oveq1d x = r A 𝑜 x + 𝑜 y = A 𝑜 r + 𝑜 y
43 42 eqeq1d x = r A 𝑜 x + 𝑜 y = B A 𝑜 r + 𝑜 y = B
44 40 43 anbi12d x = r z = x y A 𝑜 x + 𝑜 y = B z = r y A 𝑜 r + 𝑜 y = B
45 opeq2 y = s r y = r s
46 45 eqeq2d y = s z = r y z = r s
47 oveq2 y = s A 𝑜 r + 𝑜 y = A 𝑜 r + 𝑜 s
48 47 eqeq1d y = s A 𝑜 r + 𝑜 y = B A 𝑜 r + 𝑜 s = B
49 46 48 anbi12d y = s z = r y A 𝑜 r + 𝑜 y = B z = r s A 𝑜 r + 𝑜 s = B
50 44 49 cbvrex2vw x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A z = r s A 𝑜 r + 𝑜 s = B
51 eqeq1 z = t z = r s t = r s
52 51 anbi1d z = t z = r s A 𝑜 r + 𝑜 s = B t = r s A 𝑜 r + 𝑜 s = B
53 52 2rexbidv z = t r On s A z = r s A 𝑜 r + 𝑜 s = B r On s A t = r s A 𝑜 r + 𝑜 s = B
54 50 53 syl5bb z = t x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B
55 54 eu4 ∃! z x On y A z = x y A 𝑜 x + 𝑜 y = B z x On y A z = x y A 𝑜 x + 𝑜 y = B z t x On y A z = x y A 𝑜 x + 𝑜 y = B r On s A t = r s A 𝑜 r + 𝑜 s = B z = t
56 12 38 55 sylanbrc A On B On A ∃! z x On y A z = x y A 𝑜 x + 𝑜 y = B