Step | Hyp | Ref
| Expression |
1 | | eqid 2724 |
. . 3
⊢
(Base‘𝑇) =
(Base‘𝑇) |
2 | | eqid 2724 |
. . 3
⊢
(0g‘𝑇) = (0g‘𝑇) |
3 | | eqid 2724 |
. . 3
⊢
(+g‘𝑇) = (+g‘𝑇) |
4 | | eqid 2724 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
5 | | eqid 2724 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
6 | 4, 5 | mndidcl 18674 |
. . . . . 6
⊢ (𝑅 ∈ Mnd →
(0g‘𝑅)
∈ (Base‘𝑅)) |
7 | 6 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
(0g‘𝑅)
∈ (Base‘𝑅)) |
8 | | eqid 2724 |
. . . . . . 7
⊢
(Base‘𝑆) =
(Base‘𝑆) |
9 | | eqid 2724 |
. . . . . . 7
⊢
(0g‘𝑆) = (0g‘𝑆) |
10 | 8, 9 | mndidcl 18674 |
. . . . . 6
⊢ (𝑆 ∈ Mnd →
(0g‘𝑆)
∈ (Base‘𝑆)) |
11 | 10 | adantl 481 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
(0g‘𝑆)
∈ (Base‘𝑆)) |
12 | 7, 11 | opelxpd 5706 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
〈(0g‘𝑅), (0g‘𝑆)〉 ∈ ((Base‘𝑅) × (Base‘𝑆))) |
13 | | xpsmnd0.t |
. . . . 5
⊢ 𝑇 = (𝑅 ×s 𝑆) |
14 | | simpl 482 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑅 ∈ Mnd) |
15 | | simpr 484 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑆 ∈ Mnd) |
16 | 13, 4, 8, 14, 15 | xpsbas 17519 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
((Base‘𝑅) ×
(Base‘𝑆)) =
(Base‘𝑇)) |
17 | 12, 16 | eleqtrd 2827 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
〈(0g‘𝑅), (0g‘𝑆)〉 ∈ (Base‘𝑇)) |
18 | 16 | eleq2d 2811 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (𝑥 ∈ ((Base‘𝑅) × (Base‘𝑆)) ↔ 𝑥 ∈ (Base‘𝑇))) |
19 | | elxp2 5691 |
. . . . . 6
⊢ (𝑥 ∈ ((Base‘𝑅) × (Base‘𝑆)) ↔ ∃𝑎 ∈ (Base‘𝑅)∃𝑏 ∈ (Base‘𝑆)𝑥 = 〈𝑎, 𝑏〉) |
20 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → 𝑅 ∈ Mnd) |
21 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → 𝑆 ∈ Mnd) |
22 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → (0g‘𝑅) ∈ (Base‘𝑅)) |
23 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → (0g‘𝑆) ∈ (Base‘𝑆)) |
24 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆)) → 𝑎 ∈ (Base‘𝑅)) |
25 | 24 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → 𝑎 ∈ (Base‘𝑅)) |
26 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆)) → 𝑏 ∈ (Base‘𝑆)) |
27 | 26 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → 𝑏 ∈ (Base‘𝑆)) |
28 | | eqid 2724 |
. . . . . . . . . . . 12
⊢
(+g‘𝑅) = (+g‘𝑅) |
29 | 4, 28 | mndcl 18667 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Mnd ∧
(0g‘𝑅)
∈ (Base‘𝑅) ∧
𝑎 ∈ (Base‘𝑅)) →
((0g‘𝑅)(+g‘𝑅)𝑎) ∈ (Base‘𝑅)) |
30 | 20, 22, 25, 29 | syl3anc 1368 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → ((0g‘𝑅)(+g‘𝑅)𝑎) ∈ (Base‘𝑅)) |
31 | | eqid 2724 |
. . . . . . . . . . . 12
⊢
(+g‘𝑆) = (+g‘𝑆) |
32 | 8, 31 | mndcl 18667 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Mnd ∧
(0g‘𝑆)
∈ (Base‘𝑆) ∧
𝑏 ∈ (Base‘𝑆)) →
((0g‘𝑆)(+g‘𝑆)𝑏) ∈ (Base‘𝑆)) |
33 | 21, 23, 27, 32 | syl3anc 1368 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → ((0g‘𝑆)(+g‘𝑆)𝑏) ∈ (Base‘𝑆)) |
34 | 13, 4, 8, 20, 21, 22, 23, 25, 27, 30, 33, 28, 31, 3 | xpsadd 17521 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → (〈(0g‘𝑅), (0g‘𝑆)〉(+g‘𝑇)〈𝑎, 𝑏〉) = 〈((0g‘𝑅)(+g‘𝑅)𝑎), ((0g‘𝑆)(+g‘𝑆)𝑏)〉) |
35 | 4, 28, 5 | mndlid 18679 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Mnd ∧ 𝑎 ∈ (Base‘𝑅)) →
((0g‘𝑅)(+g‘𝑅)𝑎) = 𝑎) |
36 | 14, 24, 35 | syl2an 595 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → ((0g‘𝑅)(+g‘𝑅)𝑎) = 𝑎) |
37 | 8, 31, 9 | mndlid 18679 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Mnd ∧ 𝑏 ∈ (Base‘𝑆)) →
((0g‘𝑆)(+g‘𝑆)𝑏) = 𝑏) |
38 | 15, 26, 37 | syl2an 595 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → ((0g‘𝑆)(+g‘𝑆)𝑏) = 𝑏) |
39 | 36, 38 | opeq12d 4874 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → 〈((0g‘𝑅)(+g‘𝑅)𝑎), ((0g‘𝑆)(+g‘𝑆)𝑏)〉 = 〈𝑎, 𝑏〉) |
40 | 34, 39 | eqtrd 2764 |
. . . . . . . 8
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → (〈(0g‘𝑅), (0g‘𝑆)〉(+g‘𝑇)〈𝑎, 𝑏〉) = 〈𝑎, 𝑏〉) |
41 | | oveq2 7410 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑎, 𝑏〉 →
(〈(0g‘𝑅), (0g‘𝑆)〉(+g‘𝑇)𝑥) = (〈(0g‘𝑅), (0g‘𝑆)〉(+g‘𝑇)〈𝑎, 𝑏〉)) |
42 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑎, 𝑏〉 → 𝑥 = 〈𝑎, 𝑏〉) |
43 | 41, 42 | eqeq12d 2740 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑎, 𝑏〉 →
((〈(0g‘𝑅), (0g‘𝑆)〉(+g‘𝑇)𝑥) = 𝑥 ↔ (〈(0g‘𝑅), (0g‘𝑆)〉(+g‘𝑇)〈𝑎, 𝑏〉) = 〈𝑎, 𝑏〉)) |
44 | 40, 43 | syl5ibrcom 246 |
. . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → (𝑥 = 〈𝑎, 𝑏〉 →
(〈(0g‘𝑅), (0g‘𝑆)〉(+g‘𝑇)𝑥) = 𝑥)) |
45 | 44 | rexlimdvva 3203 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
(∃𝑎 ∈
(Base‘𝑅)∃𝑏 ∈ (Base‘𝑆)𝑥 = 〈𝑎, 𝑏〉 →
(〈(0g‘𝑅), (0g‘𝑆)〉(+g‘𝑇)𝑥) = 𝑥)) |
46 | 19, 45 | biimtrid 241 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (𝑥 ∈ ((Base‘𝑅) × (Base‘𝑆)) →
(〈(0g‘𝑅), (0g‘𝑆)〉(+g‘𝑇)𝑥) = 𝑥)) |
47 | 18, 46 | sylbird 260 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (𝑥 ∈ (Base‘𝑇) →
(〈(0g‘𝑅), (0g‘𝑆)〉(+g‘𝑇)𝑥) = 𝑥)) |
48 | 47 | imp 406 |
. . 3
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ 𝑥 ∈ (Base‘𝑇)) →
(〈(0g‘𝑅), (0g‘𝑆)〉(+g‘𝑇)𝑥) = 𝑥) |
49 | 4, 28 | mndcl 18667 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Mnd ∧ 𝑎 ∈ (Base‘𝑅) ∧
(0g‘𝑅)
∈ (Base‘𝑅))
→ (𝑎(+g‘𝑅)(0g‘𝑅)) ∈ (Base‘𝑅)) |
50 | 20, 25, 22, 49 | syl3anc 1368 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → (𝑎(+g‘𝑅)(0g‘𝑅)) ∈ (Base‘𝑅)) |
51 | 8, 31 | mndcl 18667 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Mnd ∧ 𝑏 ∈ (Base‘𝑆) ∧
(0g‘𝑆)
∈ (Base‘𝑆))
→ (𝑏(+g‘𝑆)(0g‘𝑆)) ∈ (Base‘𝑆)) |
52 | 21, 27, 23, 51 | syl3anc 1368 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → (𝑏(+g‘𝑆)(0g‘𝑆)) ∈ (Base‘𝑆)) |
53 | 13, 4, 8, 20, 21, 25, 27, 22, 23, 50, 52, 28, 31, 3 | xpsadd 17521 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → (〈𝑎, 𝑏〉(+g‘𝑇)〈(0g‘𝑅), (0g‘𝑆)〉) = 〈(𝑎(+g‘𝑅)(0g‘𝑅)), (𝑏(+g‘𝑆)(0g‘𝑆))〉) |
54 | 4, 28, 5 | mndrid 18680 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Mnd ∧ 𝑎 ∈ (Base‘𝑅)) → (𝑎(+g‘𝑅)(0g‘𝑅)) = 𝑎) |
55 | 14, 24, 54 | syl2an 595 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → (𝑎(+g‘𝑅)(0g‘𝑅)) = 𝑎) |
56 | 8, 31, 9 | mndrid 18680 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Mnd ∧ 𝑏 ∈ (Base‘𝑆)) → (𝑏(+g‘𝑆)(0g‘𝑆)) = 𝑏) |
57 | 15, 26, 56 | syl2an 595 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → (𝑏(+g‘𝑆)(0g‘𝑆)) = 𝑏) |
58 | 55, 57 | opeq12d 4874 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → 〈(𝑎(+g‘𝑅)(0g‘𝑅)), (𝑏(+g‘𝑆)(0g‘𝑆))〉 = 〈𝑎, 𝑏〉) |
59 | 53, 58 | eqtrd 2764 |
. . . . . . . 8
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → (〈𝑎, 𝑏〉(+g‘𝑇)〈(0g‘𝑅), (0g‘𝑆)〉) = 〈𝑎, 𝑏〉) |
60 | | oveq1 7409 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (𝑥(+g‘𝑇)〈(0g‘𝑅), (0g‘𝑆)〉) = (〈𝑎, 𝑏〉(+g‘𝑇)〈(0g‘𝑅), (0g‘𝑆)〉)) |
61 | 60, 42 | eqeq12d 2740 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑎, 𝑏〉 → ((𝑥(+g‘𝑇)〈(0g‘𝑅), (0g‘𝑆)〉) = 𝑥 ↔ (〈𝑎, 𝑏〉(+g‘𝑇)〈(0g‘𝑅), (0g‘𝑆)〉) = 〈𝑎, 𝑏〉)) |
62 | 59, 61 | syl5ibrcom 246 |
. . . . . . 7
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑆))) → (𝑥 = 〈𝑎, 𝑏〉 → (𝑥(+g‘𝑇)〈(0g‘𝑅), (0g‘𝑆)〉) = 𝑥)) |
63 | 62 | rexlimdvva 3203 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
(∃𝑎 ∈
(Base‘𝑅)∃𝑏 ∈ (Base‘𝑆)𝑥 = 〈𝑎, 𝑏〉 → (𝑥(+g‘𝑇)〈(0g‘𝑅), (0g‘𝑆)〉) = 𝑥)) |
64 | 19, 63 | biimtrid 241 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (𝑥 ∈ ((Base‘𝑅) × (Base‘𝑆)) → (𝑥(+g‘𝑇)〈(0g‘𝑅), (0g‘𝑆)〉) = 𝑥)) |
65 | 18, 64 | sylbird 260 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (𝑥 ∈ (Base‘𝑇) → (𝑥(+g‘𝑇)〈(0g‘𝑅), (0g‘𝑆)〉) = 𝑥)) |
66 | 65 | imp 406 |
. . 3
⊢ (((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) ∧ 𝑥 ∈ (Base‘𝑇)) → (𝑥(+g‘𝑇)〈(0g‘𝑅), (0g‘𝑆)〉) = 𝑥) |
67 | 1, 2, 3, 17, 48, 66 | ismgmid2 18593 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
〈(0g‘𝑅), (0g‘𝑆)〉 = (0g‘𝑇)) |
68 | 67 | eqcomd 2730 |
1
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
(0g‘𝑇) =
〈(0g‘𝑅), (0g‘𝑆)〉) |