Proof of Theorem rglcom4d
Step | Hyp | Ref
| Expression |
1 | | o2timesd.u |
. . . . . . 7
⊢ (𝜑 → 1 ∈ 𝐵) |
2 | 1, 1 | jca 512 |
. . . . . 6
⊢ (𝜑 → ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵)) |
3 | | rglcom4d.a |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) ∈ 𝐵) |
4 | | oveq1 7401 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝑥 + 𝑦) = ( 1 + 𝑦)) |
5 | 4 | eleq1d 2818 |
. . . . . . 7
⊢ (𝑥 = 1 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ ( 1 + 𝑦) ∈ 𝐵)) |
6 | | oveq2 7402 |
. . . . . . . 8
⊢ (𝑦 = 1 → ( 1 + 𝑦) = ( 1 + 1 )) |
7 | 6 | eleq1d 2818 |
. . . . . . 7
⊢ (𝑦 = 1 → (( 1 + 𝑦) ∈ 𝐵 ↔ ( 1 + 1 ) ∈ 𝐵)) |
8 | 5, 7 | rspc2v 3619 |
. . . . . 6
⊢ (( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) ∈ 𝐵 → ( 1 + 1 ) ∈ 𝐵)) |
9 | 2, 3, 8 | sylc 65 |
. . . . 5
⊢ (𝜑 → ( 1 + 1 ) ∈ 𝐵) |
10 | | o2timesd.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
11 | | rglcom4d.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
12 | 9, 10, 11 | 3jca 1128 |
. . . 4
⊢ (𝜑 → (( 1 + 1 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) |
13 | | rglcom4d.d |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) |
14 | | oveq1 7401 |
. . . . . 6
⊢ (𝑥 = ( 1 + 1 ) → (𝑥 · (𝑦 + 𝑧)) = (( 1 + 1 ) · (𝑦 + 𝑧))) |
15 | | oveq1 7401 |
. . . . . . 7
⊢ (𝑥 = ( 1 + 1 ) → (𝑥 · 𝑦) = (( 1 + 1 ) · 𝑦)) |
16 | | oveq1 7401 |
. . . . . . 7
⊢ (𝑥 = ( 1 + 1 ) → (𝑥 · 𝑧) = (( 1 + 1 ) · 𝑧)) |
17 | 15, 16 | oveq12d 7412 |
. . . . . 6
⊢ (𝑥 = ( 1 + 1 ) → ((𝑥 · 𝑦) + (𝑥 · 𝑧)) = ((( 1 + 1 ) · 𝑦) + (( 1 + 1 ) · 𝑧))) |
18 | 14, 17 | eqeq12d 2748 |
. . . . 5
⊢ (𝑥 = ( 1 + 1 ) → ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ↔ (( 1 + 1 ) · (𝑦 + 𝑧)) = ((( 1 + 1 ) · 𝑦) + (( 1 + 1 ) · 𝑧)))) |
19 | | oveq1 7401 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → (𝑦 + 𝑧) = (𝑋 + 𝑧)) |
20 | 19 | oveq2d 7410 |
. . . . . 6
⊢ (𝑦 = 𝑋 → (( 1 + 1 ) · (𝑦 + 𝑧)) = (( 1 + 1 ) · (𝑋 + 𝑧))) |
21 | | oveq2 7402 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → (( 1 + 1 ) · 𝑦) = (( 1 + 1 ) · 𝑋)) |
22 | 21 | oveq1d 7409 |
. . . . . 6
⊢ (𝑦 = 𝑋 → ((( 1 + 1 ) · 𝑦) + (( 1 + 1 ) · 𝑧)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑧))) |
23 | 20, 22 | eqeq12d 2748 |
. . . . 5
⊢ (𝑦 = 𝑋 → ((( 1 + 1 ) · (𝑦 + 𝑧)) = ((( 1 + 1 ) · 𝑦) + (( 1 + 1 ) · 𝑧)) ↔ (( 1 + 1 ) · (𝑋 + 𝑧)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑧)))) |
24 | | oveq2 7402 |
. . . . . . 7
⊢ (𝑧 = 𝑌 → (𝑋 + 𝑧) = (𝑋 + 𝑌)) |
25 | 24 | oveq2d 7410 |
. . . . . 6
⊢ (𝑧 = 𝑌 → (( 1 + 1 ) · (𝑋 + 𝑧)) = (( 1 + 1 ) · (𝑋 + 𝑌))) |
26 | | oveq2 7402 |
. . . . . . 7
⊢ (𝑧 = 𝑌 → (( 1 + 1 ) · 𝑧) = (( 1 + 1 ) · 𝑌)) |
27 | 26 | oveq2d 7410 |
. . . . . 6
⊢ (𝑧 = 𝑌 → ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑧)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌))) |
28 | 25, 27 | eqeq12d 2748 |
. . . . 5
⊢ (𝑧 = 𝑌 → ((( 1 + 1 ) · (𝑋 + 𝑧)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑧)) ↔ (( 1 + 1 ) · (𝑋 + 𝑌)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌)))) |
29 | 18, 23, 28 | rspc3v 3624 |
. . . 4
⊢ ((( 1 + 1 ) ∈
𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (( 1 + 1 ) · (𝑋 + 𝑌)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌)))) |
30 | 12, 13, 29 | sylc 65 |
. . 3
⊢ (𝜑 → (( 1 + 1 ) · (𝑋 + 𝑌)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌))) |
31 | | oveq1 7401 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 + 𝑦) = (𝑋 + 𝑦)) |
32 | 31 | eleq1d 2818 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑦) ∈ 𝐵)) |
33 | | oveq2 7402 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌)) |
34 | 33 | eleq1d 2818 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → ((𝑋 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑌) ∈ 𝐵)) |
35 | 32, 34 | rspc2va 3620 |
. . . . . 6
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
36 | 10, 11, 3, 35 | syl21anc 836 |
. . . . 5
⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵) |
37 | 1, 1, 36 | 3jca 1128 |
. . . 4
⊢ (𝜑 → ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝐵)) |
38 | | o2timesd.e |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) |
39 | 4 | oveq1d 7409 |
. . . . . 6
⊢ (𝑥 = 1 → ((𝑥 + 𝑦) · 𝑧) = (( 1 + 𝑦) · 𝑧)) |
40 | | oveq1 7401 |
. . . . . . 7
⊢ (𝑥 = 1 → (𝑥 · 𝑧) = ( 1 · 𝑧)) |
41 | 40 | oveq1d 7409 |
. . . . . 6
⊢ (𝑥 = 1 → ((𝑥 · 𝑧) + (𝑦 · 𝑧)) = (( 1 · 𝑧) + (𝑦 · 𝑧))) |
42 | 39, 41 | eqeq12d 2748 |
. . . . 5
⊢ (𝑥 = 1 → (((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) ↔ (( 1 + 𝑦) · 𝑧) = (( 1 · 𝑧) + (𝑦 · 𝑧)))) |
43 | 6 | oveq1d 7409 |
. . . . . 6
⊢ (𝑦 = 1 → (( 1 + 𝑦) · 𝑧) = (( 1 + 1 ) · 𝑧)) |
44 | | oveq1 7401 |
. . . . . . 7
⊢ (𝑦 = 1 → (𝑦 · 𝑧) = ( 1 · 𝑧)) |
45 | 44 | oveq2d 7410 |
. . . . . 6
⊢ (𝑦 = 1 → (( 1 · 𝑧) + (𝑦 · 𝑧)) = (( 1 · 𝑧) + ( 1 · 𝑧))) |
46 | 43, 45 | eqeq12d 2748 |
. . . . 5
⊢ (𝑦 = 1 → ((( 1 + 𝑦) · 𝑧) = (( 1 · 𝑧) + (𝑦 · 𝑧)) ↔ (( 1 + 1 ) · 𝑧) = (( 1 · 𝑧) + ( 1 · 𝑧)))) |
47 | | oveq2 7402 |
. . . . . 6
⊢ (𝑧 = (𝑋 + 𝑌) → (( 1 + 1 ) · 𝑧) = (( 1 + 1 ) · (𝑋 + 𝑌))) |
48 | | oveq2 7402 |
. . . . . . 7
⊢ (𝑧 = (𝑋 + 𝑌) → ( 1 · 𝑧) = ( 1 · (𝑋 + 𝑌))) |
49 | 48, 48 | oveq12d 7412 |
. . . . . 6
⊢ (𝑧 = (𝑋 + 𝑌) → (( 1 · 𝑧) + ( 1 · 𝑧)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌)))) |
50 | 47, 49 | eqeq12d 2748 |
. . . . 5
⊢ (𝑧 = (𝑋 + 𝑌) → ((( 1 + 1 ) · 𝑧) = (( 1 · 𝑧) + ( 1 · 𝑧)) ↔ (( 1 + 1 ) · (𝑋 + 𝑌)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌))))) |
51 | 42, 46, 50 | rspc3v 3624 |
. . . 4
⊢ (( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) → (( 1 + 1 ) · (𝑋 + 𝑌)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌))))) |
52 | 37, 38, 51 | sylc 65 |
. . 3
⊢ (𝜑 → (( 1 + 1 ) · (𝑋 + 𝑌)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌)))) |
53 | 30, 52 | eqtr3d 2774 |
. 2
⊢ (𝜑 → ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌)))) |
54 | | o2timesd.i |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ( 1 · 𝑥) = 𝑥) |
55 | 38, 1, 54, 10 | o2timesd 19993 |
. . . 4
⊢ (𝜑 → (𝑋 + 𝑋) = (( 1 + 1 ) · 𝑋)) |
56 | 55 | eqcomd 2738 |
. . 3
⊢ (𝜑 → (( 1 + 1 ) · 𝑋) = (𝑋 + 𝑋)) |
57 | 38, 1, 54, 11 | o2timesd 19993 |
. . . 4
⊢ (𝜑 → (𝑌 + 𝑌) = (( 1 + 1 ) · 𝑌)) |
58 | 57 | eqcomd 2738 |
. . 3
⊢ (𝜑 → (( 1 + 1 ) · 𝑌) = (𝑌 + 𝑌)) |
59 | 56, 58 | oveq12d 7412 |
. 2
⊢ (𝜑 → ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌)) = ((𝑋 + 𝑋) + (𝑌 + 𝑌))) |
60 | | oveq2 7402 |
. . . . . 6
⊢ (𝑥 = (𝑋 + 𝑌) → ( 1 · 𝑥) = ( 1 · (𝑋 + 𝑌))) |
61 | | id 22 |
. . . . . 6
⊢ (𝑥 = (𝑋 + 𝑌) → 𝑥 = (𝑋 + 𝑌)) |
62 | 60, 61 | eqeq12d 2748 |
. . . . 5
⊢ (𝑥 = (𝑋 + 𝑌) → (( 1 · 𝑥) = 𝑥 ↔ ( 1 · (𝑋 + 𝑌)) = (𝑋 + 𝑌))) |
63 | 62 | rspcva 3608 |
. . . 4
⊢ (((𝑋 + 𝑌) ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ( 1 · 𝑥) = 𝑥) → ( 1 · (𝑋 + 𝑌)) = (𝑋 + 𝑌)) |
64 | 36, 54, 63 | syl2anc 584 |
. . 3
⊢ (𝜑 → ( 1 · (𝑋 + 𝑌)) = (𝑋 + 𝑌)) |
65 | 64, 64 | oveq12d 7412 |
. 2
⊢ (𝜑 → (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌))) = ((𝑋 + 𝑌) + (𝑋 + 𝑌))) |
66 | 53, 59, 65 | 3eqtr3d 2780 |
1
⊢ (𝜑 → ((𝑋 + 𝑋) + (𝑌 + 𝑌)) = ((𝑋 + 𝑌) + (𝑋 + 𝑌))) |