| Step | Hyp | Ref
| Expression |
|---|
| 1 | | xpsgrp.t |
. . 3
⊢ 𝑇 = (𝑅 ×s 𝑆) |
| 2 | | eqid 2740 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 3 | | eqid 2740 |
. . 3
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 4 | | simpl 482 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) → 𝑅 ∈ Grp) |
| 5 | | simpr 484 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) → 𝑆 ∈ Grp) |
| 6 | | eqid 2740 |
. . 3
⊢ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) |
| 7 | | eqid 2740 |
. . 3
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
| 8 | | eqid 2740 |
. . 3
⊢
((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) = ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) |
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsval 17632 |
. 2
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) → 𝑇 = (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
“s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) |
| 10 | 6 | xpsff1o2 17631 |
. . . . 5
⊢ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→ran
(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) |
| 11 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsrnbas 17633 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) → ran (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) =
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) |
| 12 | 11 | f1oeq3d 6861 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) → ((𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→ran
(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) ↔ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})))) |
| 13 | 10, 12 | mpbii 233 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) → (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) |
| 14 | | f1ocnv 6876 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) → ◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))–1-1-onto→((Base‘𝑅) × (Base‘𝑆))) |
| 15 | | f1of1 6863 |
. . . 4
⊢ (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))–1-1-onto→((Base‘𝑅) × (Base‘𝑆)) → ◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))–1-1→((Base‘𝑅) × (Base‘𝑆))) |
| 16 | 13, 14, 15 | 3syl 18 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) → ◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))–1-1→((Base‘𝑅) × (Base‘𝑆))) |
| 17 | | 2on 8538 |
. . . . 5
⊢
2o ∈ On |
| 18 | 17 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) →
2o ∈ On) |
| 19 | | fvexd 6937 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) →
(Scalar‘𝑅) ∈
V) |
| 20 | | xpscf 17627 |
. . . . 5
⊢
({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}:2o⟶Grp
↔ (𝑅 ∈ Grp ∧
𝑆 ∈
Grp)) |
| 21 | 20 | biimpri 228 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) →
{⟨∅, 𝑅⟩,
⟨1o, 𝑆⟩}:2o⟶Grp) |
| 22 | 8, 18, 19, 21 | prdsgrpd 19092 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) →
((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o,
𝑆⟩}) ∈
Grp) |
| 23 | | eqid 2740 |
. . . 4
⊢ (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
“s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) = (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
“s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) |
| 24 | | eqid 2740 |
. . . 4
⊢
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) =
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) |
| 25 | 23, 24 | imasgrpf1 19099 |
. . 3
⊢ ((◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))–1-1→((Base‘𝑅) × (Base‘𝑆)) ∧ ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) ∈ Grp) →
(◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
“s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∈
Grp) |
| 26 | 16, 22, 25 | syl2anc 583 |
. 2
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) → (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
“s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∈
Grp) |
| 27 | 9, 26 | eqeltrd 2844 |
1
⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) → 𝑇 ∈ Grp) |
