Proof of Theorem pwsmgp
Step | Hyp | Ref
| Expression |
1 | | eqid 2760 |
. . . . . 6
⊢
((Scalar‘𝑅)Xs(𝐼 × {𝑅})) = ((Scalar‘𝑅)Xs(𝐼 × {𝑅})) |
2 | | eqid 2760 |
. . . . . 6
⊢
(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = (mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
3 | | eqid 2760 |
. . . . . 6
⊢
((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))) = ((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))) |
4 | | simpr 479 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐼 ∈ 𝑊) |
5 | | fvexd 6364 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Scalar‘𝑅) ∈ V) |
6 | | fnconstg 6254 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑉 → (𝐼 × {𝑅}) Fn 𝐼) |
7 | 6 | adantr 472 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐼 × {𝑅}) Fn 𝐼) |
8 | 1, 2, 3, 4, 5, 7 | prdsmgp 18810 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) →
((Base‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) = (Base‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))) ∧
(+g‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) =
(+g‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))))) |
9 | 8 | simpld 477 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) →
(Base‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) = (Base‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))))) |
10 | | pwsmgp.n |
. . . . . 6
⊢ 𝑁 = (mulGrp‘𝑌) |
11 | | pwsmgp.y |
. . . . . . . 8
⊢ 𝑌 = (𝑅 ↑s 𝐼) |
12 | | eqid 2760 |
. . . . . . . 8
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
13 | 11, 12 | pwsval 16348 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑌 = ((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
14 | 13 | fveq2d 6356 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (mulGrp‘𝑌) = (mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
15 | 10, 14 | syl5eq 2806 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑁 = (mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
16 | 15 | fveq2d 6356 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝑁) =
(Base‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))) |
17 | | pwsmgp.z |
. . . . . 6
⊢ 𝑍 = (𝑀 ↑s 𝐼) |
18 | | pwsmgp.m |
. . . . . . . . 9
⊢ 𝑀 = (mulGrp‘𝑅) |
19 | | fvex 6362 |
. . . . . . . . 9
⊢
(mulGrp‘𝑅)
∈ V |
20 | 18, 19 | eqeltri 2835 |
. . . . . . . 8
⊢ 𝑀 ∈ V |
21 | | eqid 2760 |
. . . . . . . . 9
⊢ (𝑀 ↑s 𝐼) = (𝑀 ↑s 𝐼) |
22 | | eqid 2760 |
. . . . . . . . 9
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
23 | 21, 22 | pwsval 16348 |
. . . . . . . 8
⊢ ((𝑀 ∈ V ∧ 𝐼 ∈ 𝑊) → (𝑀 ↑s 𝐼) = ((Scalar‘𝑀)Xs(𝐼 × {𝑀}))) |
24 | 20, 4, 23 | sylancr 698 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑀 ↑s 𝐼) = ((Scalar‘𝑀)Xs(𝐼 × {𝑀}))) |
25 | 18, 12 | mgpsca 18696 |
. . . . . . . . . 10
⊢
(Scalar‘𝑅) =
(Scalar‘𝑀) |
26 | 25 | eqcomi 2769 |
. . . . . . . . 9
⊢
(Scalar‘𝑀) =
(Scalar‘𝑅) |
27 | 26 | a1i 11 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Scalar‘𝑀) = (Scalar‘𝑅)) |
28 | | fnmgp 18691 |
. . . . . . . . . 10
⊢ mulGrp Fn
V |
29 | | elex 3352 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
30 | 29 | adantr 472 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑅 ∈ V) |
31 | | fcoconst 6564 |
. . . . . . . . . 10
⊢ ((mulGrp
Fn V ∧ 𝑅 ∈ V)
→ (mulGrp ∘ (𝐼
× {𝑅})) = (𝐼 × {(mulGrp‘𝑅)})) |
32 | 28, 30, 31 | sylancr 698 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (mulGrp ∘ (𝐼 × {𝑅})) = (𝐼 × {(mulGrp‘𝑅)})) |
33 | 18 | sneqi 4332 |
. . . . . . . . . 10
⊢ {𝑀} = {(mulGrp‘𝑅)} |
34 | 33 | xpeq2i 5293 |
. . . . . . . . 9
⊢ (𝐼 × {𝑀}) = (𝐼 × {(mulGrp‘𝑅)}) |
35 | 32, 34 | syl6reqr 2813 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐼 × {𝑀}) = (mulGrp ∘ (𝐼 × {𝑅}))) |
36 | 27, 35 | oveq12d 6831 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ((Scalar‘𝑀)Xs(𝐼 × {𝑀})) = ((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))) |
37 | 24, 36 | eqtrd 2794 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑀 ↑s 𝐼) = ((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))) |
38 | 17, 37 | syl5eq 2806 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑍 = ((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))) |
39 | 38 | fveq2d 6356 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝑍) = (Base‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))))) |
40 | 9, 16, 39 | 3eqtr4d 2804 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝑁) = (Base‘𝑍)) |
41 | | pwsmgp.b |
. . 3
⊢ 𝐵 = (Base‘𝑁) |
42 | | pwsmgp.c |
. . 3
⊢ 𝐶 = (Base‘𝑍) |
43 | 40, 41, 42 | 3eqtr4g 2819 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐵 = 𝐶) |
44 | 8 | simprd 482 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) →
(+g‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) =
(+g‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))))) |
45 | 15 | fveq2d 6356 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (+g‘𝑁) =
(+g‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))) |
46 | 38 | fveq2d 6356 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (+g‘𝑍) =
(+g‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))))) |
47 | 44, 45, 46 | 3eqtr4d 2804 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (+g‘𝑁) = (+g‘𝑍)) |
48 | | pwsmgp.p |
. . 3
⊢ + =
(+g‘𝑁) |
49 | | pwsmgp.q |
. . 3
⊢ ✚ =
(+g‘𝑍) |
50 | 47, 48, 49 | 3eqtr4g 2819 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → + = ✚ ) |
51 | 43, 50 | jca 555 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐵 = 𝐶 ∧ + = ✚ )) |