| Step |
Hyp |
Ref |
Expression |
| 1 |
|
oveq1 |
⊢ ( 𝑎 = 𝑐 → ( 𝑎 ·no 𝑏 ) = ( 𝑐 ·no 𝑏 ) ) |
| 2 |
|
oveq2 |
⊢ ( 𝑎 = 𝑐 → ( 𝑏 ·no 𝑎 ) = ( 𝑏 ·no 𝑐 ) ) |
| 3 |
1 2
|
eqeq12d |
⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 ·no 𝑏 ) = ( 𝑏 ·no 𝑎 ) ↔ ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ) ) |
| 4 |
|
oveq2 |
⊢ ( 𝑏 = 𝑑 → ( 𝑐 ·no 𝑏 ) = ( 𝑐 ·no 𝑑 ) ) |
| 5 |
|
oveq1 |
⊢ ( 𝑏 = 𝑑 → ( 𝑏 ·no 𝑐 ) = ( 𝑑 ·no 𝑐 ) ) |
| 6 |
4 5
|
eqeq12d |
⊢ ( 𝑏 = 𝑑 → ( ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ↔ ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ) ) |
| 7 |
|
oveq1 |
⊢ ( 𝑎 = 𝑐 → ( 𝑎 ·no 𝑑 ) = ( 𝑐 ·no 𝑑 ) ) |
| 8 |
|
oveq2 |
⊢ ( 𝑎 = 𝑐 → ( 𝑑 ·no 𝑎 ) = ( 𝑑 ·no 𝑐 ) ) |
| 9 |
7 8
|
eqeq12d |
⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ↔ ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ) ) |
| 10 |
|
oveq1 |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 ·no 𝑏 ) = ( 𝐴 ·no 𝑏 ) ) |
| 11 |
|
oveq2 |
⊢ ( 𝑎 = 𝐴 → ( 𝑏 ·no 𝑎 ) = ( 𝑏 ·no 𝐴 ) ) |
| 12 |
10 11
|
eqeq12d |
⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ·no 𝑏 ) = ( 𝑏 ·no 𝑎 ) ↔ ( 𝐴 ·no 𝑏 ) = ( 𝑏 ·no 𝐴 ) ) ) |
| 13 |
|
oveq2 |
⊢ ( 𝑏 = 𝐵 → ( 𝐴 ·no 𝑏 ) = ( 𝐴 ·no 𝐵 ) ) |
| 14 |
|
oveq1 |
⊢ ( 𝑏 = 𝐵 → ( 𝑏 ·no 𝐴 ) = ( 𝐵 ·no 𝐴 ) ) |
| 15 |
13 14
|
eqeq12d |
⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ·no 𝑏 ) = ( 𝑏 ·no 𝐴 ) ↔ ( 𝐴 ·no 𝐵 ) = ( 𝐵 ·no 𝐴 ) ) ) |
| 16 |
|
oveq1 |
⊢ ( 𝑐 = 𝑧 → ( 𝑐 ·no 𝑏 ) = ( 𝑧 ·no 𝑏 ) ) |
| 17 |
|
oveq2 |
⊢ ( 𝑐 = 𝑧 → ( 𝑏 ·no 𝑐 ) = ( 𝑏 ·no 𝑧 ) ) |
| 18 |
16 17
|
eqeq12d |
⊢ ( 𝑐 = 𝑧 → ( ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ↔ ( 𝑧 ·no 𝑏 ) = ( 𝑏 ·no 𝑧 ) ) ) |
| 19 |
|
simplr2 |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ) |
| 20 |
|
simprl |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → 𝑧 ∈ 𝑎 ) |
| 21 |
18 19 20
|
rspcdva |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ( 𝑧 ·no 𝑏 ) = ( 𝑏 ·no 𝑧 ) ) |
| 22 |
|
oveq2 |
⊢ ( 𝑑 = 𝑦 → ( 𝑎 ·no 𝑑 ) = ( 𝑎 ·no 𝑦 ) ) |
| 23 |
|
oveq1 |
⊢ ( 𝑑 = 𝑦 → ( 𝑑 ·no 𝑎 ) = ( 𝑦 ·no 𝑎 ) ) |
| 24 |
22 23
|
eqeq12d |
⊢ ( 𝑑 = 𝑦 → ( ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ↔ ( 𝑎 ·no 𝑦 ) = ( 𝑦 ·no 𝑎 ) ) ) |
| 25 |
|
simplr3 |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) |
| 26 |
|
simprr |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → 𝑦 ∈ 𝑏 ) |
| 27 |
24 25 26
|
rspcdva |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ( 𝑎 ·no 𝑦 ) = ( 𝑦 ·no 𝑎 ) ) |
| 28 |
21 27
|
oveq12d |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ( ( 𝑧 ·no 𝑏 ) +no ( 𝑎 ·no 𝑦 ) ) = ( ( 𝑏 ·no 𝑧 ) +no ( 𝑦 ·no 𝑎 ) ) ) |
| 29 |
|
simpllr |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → 𝑏 ∈ On ) |
| 30 |
|
simplll |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → 𝑎 ∈ On ) |
| 31 |
|
onelon |
⊢ ( ( 𝑎 ∈ On ∧ 𝑧 ∈ 𝑎 ) → 𝑧 ∈ On ) |
| 32 |
30 20 31
|
syl2anc |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → 𝑧 ∈ On ) |
| 33 |
|
nmulcl |
⊢ ( ( 𝑏 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑏 ·no 𝑧 ) ∈ On ) |
| 34 |
29 32 33
|
syl2anc |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ( 𝑏 ·no 𝑧 ) ∈ On ) |
| 35 |
|
onelon |
⊢ ( ( 𝑏 ∈ On ∧ 𝑦 ∈ 𝑏 ) → 𝑦 ∈ On ) |
| 36 |
29 26 35
|
syl2anc |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → 𝑦 ∈ On ) |
| 37 |
|
nmulcl |
⊢ ( ( 𝑦 ∈ On ∧ 𝑎 ∈ On ) → ( 𝑦 ·no 𝑎 ) ∈ On ) |
| 38 |
36 30 37
|
syl2anc |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ( 𝑦 ·no 𝑎 ) ∈ On ) |
| 39 |
|
naddcom |
⊢ ( ( ( 𝑏 ·no 𝑧 ) ∈ On ∧ ( 𝑦 ·no 𝑎 ) ∈ On ) → ( ( 𝑏 ·no 𝑧 ) +no ( 𝑦 ·no 𝑎 ) ) = ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ) |
| 40 |
34 38 39
|
syl2anc |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ( ( 𝑏 ·no 𝑧 ) +no ( 𝑦 ·no 𝑎 ) ) = ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ) |
| 41 |
28 40
|
eqtrd |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ( ( 𝑧 ·no 𝑏 ) +no ( 𝑎 ·no 𝑦 ) ) = ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ) |
| 42 |
|
oveq1 |
⊢ ( 𝑐 = 𝑧 → ( 𝑐 ·no 𝑑 ) = ( 𝑧 ·no 𝑑 ) ) |
| 43 |
|
oveq2 |
⊢ ( 𝑐 = 𝑧 → ( 𝑑 ·no 𝑐 ) = ( 𝑑 ·no 𝑧 ) ) |
| 44 |
42 43
|
eqeq12d |
⊢ ( 𝑐 = 𝑧 → ( ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ↔ ( 𝑧 ·no 𝑑 ) = ( 𝑑 ·no 𝑧 ) ) ) |
| 45 |
|
oveq2 |
⊢ ( 𝑑 = 𝑦 → ( 𝑧 ·no 𝑑 ) = ( 𝑧 ·no 𝑦 ) ) |
| 46 |
|
oveq1 |
⊢ ( 𝑑 = 𝑦 → ( 𝑑 ·no 𝑧 ) = ( 𝑦 ·no 𝑧 ) ) |
| 47 |
45 46
|
eqeq12d |
⊢ ( 𝑑 = 𝑦 → ( ( 𝑧 ·no 𝑑 ) = ( 𝑑 ·no 𝑧 ) ↔ ( 𝑧 ·no 𝑦 ) = ( 𝑦 ·no 𝑧 ) ) ) |
| 48 |
|
simplr1 |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ) |
| 49 |
44 47 48 20 26
|
rspc2dv |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ( 𝑧 ·no 𝑦 ) = ( 𝑦 ·no 𝑧 ) ) |
| 50 |
49
|
oveq2d |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ( 𝑥 +no ( 𝑧 ·no 𝑦 ) ) = ( 𝑥 +no ( 𝑦 ·no 𝑧 ) ) ) |
| 51 |
41 50
|
eleq12d |
⊢ ( ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑦 ∈ 𝑏 ) ) → ( ( ( 𝑧 ·no 𝑏 ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑧 ·no 𝑦 ) ) ↔ ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ∈ ( 𝑥 +no ( 𝑦 ·no 𝑧 ) ) ) ) |
| 52 |
51
|
2ralbidva |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) → ( ∀ 𝑧 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑧 ·no 𝑏 ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑧 ·no 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ∈ ( 𝑥 +no ( 𝑦 ·no 𝑧 ) ) ) ) |
| 53 |
|
ralcom |
⊢ ( ∀ 𝑧 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ∈ ( 𝑥 +no ( 𝑦 ·no 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑎 ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ∈ ( 𝑥 +no ( 𝑦 ·no 𝑧 ) ) ) |
| 54 |
52 53
|
bitrdi |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) → ( ∀ 𝑧 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑧 ·no 𝑏 ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑧 ·no 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑎 ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ∈ ( 𝑥 +no ( 𝑦 ·no 𝑧 ) ) ) ) |
| 55 |
54
|
rabbidv |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) → { 𝑥 ∈ On ∣ ∀ 𝑧 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑧 ·no 𝑏 ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑧 ·no 𝑦 ) ) } = { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑎 ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ∈ ( 𝑥 +no ( 𝑦 ·no 𝑧 ) ) } ) |
| 56 |
55
|
inteqd |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑧 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑧 ·no 𝑏 ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑧 ·no 𝑦 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑎 ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ∈ ( 𝑥 +no ( 𝑦 ·no 𝑧 ) ) } ) |
| 57 |
|
nmulval |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑎 ·no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑧 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑧 ·no 𝑏 ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑧 ·no 𝑦 ) ) } ) |
| 58 |
57
|
adantr |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) → ( 𝑎 ·no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑧 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑧 ·no 𝑏 ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑧 ·no 𝑦 ) ) } ) |
| 59 |
|
nmulval |
⊢ ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) → ( 𝑏 ·no 𝑎 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑎 ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ∈ ( 𝑥 +no ( 𝑦 ·no 𝑧 ) ) } ) |
| 60 |
59
|
ancoms |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑏 ·no 𝑎 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑎 ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ∈ ( 𝑥 +no ( 𝑦 ·no 𝑧 ) ) } ) |
| 61 |
60
|
adantr |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) → ( 𝑏 ·no 𝑎 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑎 ( ( 𝑦 ·no 𝑎 ) +no ( 𝑏 ·no 𝑧 ) ) ∈ ( 𝑥 +no ( 𝑦 ·no 𝑧 ) ) } ) |
| 62 |
56 58 61
|
3eqtr4d |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) ) → ( 𝑎 ·no 𝑏 ) = ( 𝑏 ·no 𝑎 ) ) |
| 63 |
62
|
ex |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 ·no 𝑑 ) = ( 𝑑 ·no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 ·no 𝑏 ) = ( 𝑏 ·no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 ·no 𝑑 ) = ( 𝑑 ·no 𝑎 ) ) → ( 𝑎 ·no 𝑏 ) = ( 𝑏 ·no 𝑎 ) ) ) |
| 64 |
3 6 9 12 15 63
|
on2ind |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·no 𝐵 ) = ( 𝐵 ·no 𝐴 ) ) |