Proof of Theorem pwsmgp
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . . 6
⊢
((Scalar‘𝑅)Xs(𝐼 × {𝑅})) = ((Scalar‘𝑅)Xs(𝐼 × {𝑅})) | 
| 2 |  | eqid 2736 | . . . . . 6
⊢
(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = (mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) | 
| 3 |  | eqid 2736 | . . . . . 6
⊢
((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))) = ((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))) | 
| 4 |  | simpr 484 | . . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐼 ∈ 𝑊) | 
| 5 |  | fvexd 6920 | . . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Scalar‘𝑅) ∈ V) | 
| 6 |  | fnconstg 6795 | . . . . . . 7
⊢ (𝑅 ∈ 𝑉 → (𝐼 × {𝑅}) Fn 𝐼) | 
| 7 | 6 | adantr 480 | . . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐼 × {𝑅}) Fn 𝐼) | 
| 8 | 1, 2, 3, 4, 5, 7 | prdsmgp 20149 | . . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) →
((Base‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) = (Base‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))) ∧
(+g‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) =
(+g‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))))) | 
| 9 | 8 | simpld 494 | . . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) →
(Base‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) = (Base‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))))) | 
| 10 |  | pwsmgp.n | . . . . . 6
⊢ 𝑁 = (mulGrp‘𝑌) | 
| 11 |  | pwsmgp.y | . . . . . . . 8
⊢ 𝑌 = (𝑅 ↑s 𝐼) | 
| 12 |  | eqid 2736 | . . . . . . . 8
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) | 
| 13 | 11, 12 | pwsval 17532 | . . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑌 = ((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) | 
| 14 | 13 | fveq2d 6909 | . . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (mulGrp‘𝑌) = (mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) | 
| 15 | 10, 14 | eqtrid 2788 | . . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑁 = (mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) | 
| 16 | 15 | fveq2d 6909 | . . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝑁) =
(Base‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))) | 
| 17 |  | pwsmgp.z | . . . . . 6
⊢ 𝑍 = (𝑀 ↑s 𝐼) | 
| 18 |  | pwsmgp.m | . . . . . . . . 9
⊢ 𝑀 = (mulGrp‘𝑅) | 
| 19 | 18 | fvexi 6919 | . . . . . . . 8
⊢ 𝑀 ∈ V | 
| 20 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑀 ↑s 𝐼) = (𝑀 ↑s 𝐼) | 
| 21 |  | eqid 2736 | . . . . . . . . 9
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) | 
| 22 | 20, 21 | pwsval 17532 | . . . . . . . 8
⊢ ((𝑀 ∈ V ∧ 𝐼 ∈ 𝑊) → (𝑀 ↑s 𝐼) = ((Scalar‘𝑀)Xs(𝐼 × {𝑀}))) | 
| 23 | 19, 4, 22 | sylancr 587 | . . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑀 ↑s 𝐼) = ((Scalar‘𝑀)Xs(𝐼 × {𝑀}))) | 
| 24 | 18, 12 | mgpsca 20144 | . . . . . . . . . 10
⊢
(Scalar‘𝑅) =
(Scalar‘𝑀) | 
| 25 | 24 | eqcomi 2745 | . . . . . . . . 9
⊢
(Scalar‘𝑀) =
(Scalar‘𝑅) | 
| 26 | 25 | a1i 11 | . . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Scalar‘𝑀) = (Scalar‘𝑅)) | 
| 27 | 18 | sneqi 4636 | . . . . . . . . . 10
⊢ {𝑀} = {(mulGrp‘𝑅)} | 
| 28 | 27 | xpeq2i 5711 | . . . . . . . . 9
⊢ (𝐼 × {𝑀}) = (𝐼 × {(mulGrp‘𝑅)}) | 
| 29 |  | fnmgp 20140 | . . . . . . . . . 10
⊢ mulGrp Fn
V | 
| 30 |  | elex 3500 | . . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) | 
| 31 | 30 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑅 ∈ V) | 
| 32 |  | fcoconst 7153 | . . . . . . . . . 10
⊢ ((mulGrp
Fn V ∧ 𝑅 ∈ V)
→ (mulGrp ∘ (𝐼
× {𝑅})) = (𝐼 × {(mulGrp‘𝑅)})) | 
| 33 | 29, 31, 32 | sylancr 587 | . . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (mulGrp ∘ (𝐼 × {𝑅})) = (𝐼 × {(mulGrp‘𝑅)})) | 
| 34 | 28, 33 | eqtr4id 2795 | . . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐼 × {𝑀}) = (mulGrp ∘ (𝐼 × {𝑅}))) | 
| 35 | 26, 34 | oveq12d 7450 | . . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ((Scalar‘𝑀)Xs(𝐼 × {𝑀})) = ((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))) | 
| 36 | 23, 35 | eqtrd 2776 | . . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑀 ↑s 𝐼) = ((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))) | 
| 37 | 17, 36 | eqtrid 2788 | . . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑍 = ((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))) | 
| 38 | 37 | fveq2d 6909 | . . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝑍) = (Base‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))))) | 
| 39 | 9, 16, 38 | 3eqtr4d 2786 | . . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝑁) = (Base‘𝑍)) | 
| 40 |  | pwsmgp.b | . . 3
⊢ 𝐵 = (Base‘𝑁) | 
| 41 |  | pwsmgp.c | . . 3
⊢ 𝐶 = (Base‘𝑍) | 
| 42 | 39, 40, 41 | 3eqtr4g 2801 | . 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐵 = 𝐶) | 
| 43 | 8 | simprd 495 | . . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) →
(+g‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) =
(+g‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))))) | 
| 44 | 15 | fveq2d 6909 | . . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (+g‘𝑁) =
(+g‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))) | 
| 45 | 37 | fveq2d 6909 | . . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (+g‘𝑍) =
(+g‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))))) | 
| 46 | 43, 44, 45 | 3eqtr4d 2786 | . . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (+g‘𝑁) = (+g‘𝑍)) | 
| 47 |  | pwsmgp.p | . . 3
⊢  + =
(+g‘𝑁) | 
| 48 |  | pwsmgp.q | . . 3
⊢  ✚ =
(+g‘𝑍) | 
| 49 | 46, 47, 48 | 3eqtr4g 2801 | . 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → + = ✚ ) | 
| 50 | 42, 49 | jca 511 | 1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐵 = 𝐶 ∧ + = ✚ )) |