Proof of Theorem pwsmgp
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . 6
⊢
((Scalar‘𝑅)Xs(𝐼 × {𝑅})) = ((Scalar‘𝑅)Xs(𝐼 × {𝑅})) |
2 | | eqid 2610 |
. . . . . 6
⊢
(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = (mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
3 | | eqid 2610 |
. . . . . 6
⊢
((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))) = ((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))) |
4 | | simpr 476 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐼 ∈ 𝑊) |
5 | | fvex 6113 |
. . . . . . 7
⊢
(Scalar‘𝑅)
∈ V |
6 | 5 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Scalar‘𝑅) ∈ V) |
7 | | fnconstg 6006 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑉 → (𝐼 × {𝑅}) Fn 𝐼) |
8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐼 × {𝑅}) Fn 𝐼) |
9 | 1, 2, 3, 4, 6, 8 | prdsmgp 18433 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) →
((Base‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) = (Base‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))) ∧
(+g‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) =
(+g‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))))) |
10 | 9 | simpld 474 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) →
(Base‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) = (Base‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))))) |
11 | | pwsmgp.n |
. . . . . 6
⊢ 𝑁 = (mulGrp‘𝑌) |
12 | | pwsmgp.y |
. . . . . . . 8
⊢ 𝑌 = (𝑅 ↑s 𝐼) |
13 | | eqid 2610 |
. . . . . . . 8
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
14 | 12, 13 | pwsval 15969 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑌 = ((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
15 | 14 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (mulGrp‘𝑌) = (mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
16 | 11, 15 | syl5eq 2656 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑁 = (mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
17 | 16 | fveq2d 6107 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝑁) =
(Base‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))) |
18 | | pwsmgp.z |
. . . . . 6
⊢ 𝑍 = (𝑀 ↑s 𝐼) |
19 | | pwsmgp.m |
. . . . . . . . 9
⊢ 𝑀 = (mulGrp‘𝑅) |
20 | | fvex 6113 |
. . . . . . . . 9
⊢
(mulGrp‘𝑅)
∈ V |
21 | 19, 20 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑀 ∈ V |
22 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑀 ↑s 𝐼) = (𝑀 ↑s 𝐼) |
23 | | eqid 2610 |
. . . . . . . . 9
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
24 | 22, 23 | pwsval 15969 |
. . . . . . . 8
⊢ ((𝑀 ∈ V ∧ 𝐼 ∈ 𝑊) → (𝑀 ↑s 𝐼) = ((Scalar‘𝑀)Xs(𝐼 × {𝑀}))) |
25 | 21, 4, 24 | sylancr 694 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑀 ↑s 𝐼) = ((Scalar‘𝑀)Xs(𝐼 × {𝑀}))) |
26 | 19, 13 | mgpsca 18319 |
. . . . . . . . . 10
⊢
(Scalar‘𝑅) =
(Scalar‘𝑀) |
27 | 26 | eqcomi 2619 |
. . . . . . . . 9
⊢
(Scalar‘𝑀) =
(Scalar‘𝑅) |
28 | 27 | a1i 11 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Scalar‘𝑀) = (Scalar‘𝑅)) |
29 | | fnmgp 18314 |
. . . . . . . . . 10
⊢ mulGrp Fn
V |
30 | | elex 3185 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
31 | 30 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑅 ∈ V) |
32 | | fcoconst 6307 |
. . . . . . . . . 10
⊢ ((mulGrp
Fn V ∧ 𝑅 ∈ V)
→ (mulGrp ∘ (𝐼
× {𝑅})) = (𝐼 × {(mulGrp‘𝑅)})) |
33 | 29, 31, 32 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (mulGrp ∘ (𝐼 × {𝑅})) = (𝐼 × {(mulGrp‘𝑅)})) |
34 | 19 | sneqi 4136 |
. . . . . . . . . 10
⊢ {𝑀} = {(mulGrp‘𝑅)} |
35 | 34 | xpeq2i 5060 |
. . . . . . . . 9
⊢ (𝐼 × {𝑀}) = (𝐼 × {(mulGrp‘𝑅)}) |
36 | 33, 35 | syl6reqr 2663 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐼 × {𝑀}) = (mulGrp ∘ (𝐼 × {𝑅}))) |
37 | 28, 36 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ((Scalar‘𝑀)Xs(𝐼 × {𝑀})) = ((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))) |
38 | 25, 37 | eqtrd 2644 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑀 ↑s 𝐼) = ((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))) |
39 | 18, 38 | syl5eq 2656 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑍 = ((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅})))) |
40 | 39 | fveq2d 6107 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝑍) = (Base‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))))) |
41 | 10, 17, 40 | 3eqtr4d 2654 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝑁) = (Base‘𝑍)) |
42 | | pwsmgp.b |
. . 3
⊢ 𝐵 = (Base‘𝑁) |
43 | | pwsmgp.c |
. . 3
⊢ 𝐶 = (Base‘𝑍) |
44 | 41, 42, 43 | 3eqtr4g 2669 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐵 = 𝐶) |
45 | 9 | simprd 478 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) →
(+g‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) =
(+g‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))))) |
46 | 16 | fveq2d 6107 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (+g‘𝑁) =
(+g‘(mulGrp‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))) |
47 | 39 | fveq2d 6107 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (+g‘𝑍) =
(+g‘((Scalar‘𝑅)Xs(mulGrp ∘ (𝐼 × {𝑅}))))) |
48 | 45, 46, 47 | 3eqtr4d 2654 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (+g‘𝑁) = (+g‘𝑍)) |
49 | | pwsmgp.p |
. . 3
⊢ + =
(+g‘𝑁) |
50 | | pwsmgp.q |
. . 3
⊢ ✚ =
(+g‘𝑍) |
51 | 48, 49, 50 | 3eqtr4g 2669 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → + = ✚ ) |
52 | 44, 51 | jca 553 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐵 = 𝐶 ∧ + = ✚ )) |