Proof of Theorem mgpress
Step | Hyp | Ref
| Expression |
1 | | mgpress.2 |
. . 3
⊢ 𝑀 = (mulGrp‘𝑅) |
2 | | simpr 477 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ (Base‘𝑅) ⊆ 𝐴) → (Base‘𝑅) ⊆ 𝐴) |
3 | | fvex 6201 |
. . . . . 6
⊢
(mulGrp‘𝑅)
∈ V |
4 | 1, 3 | eqeltri 2697 |
. . . . 5
⊢ 𝑀 ∈ V |
5 | 4 | a1i 11 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ (Base‘𝑅) ⊆ 𝐴) → 𝑀 ∈ V) |
6 | | simplr 792 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ (Base‘𝑅) ⊆ 𝐴) → 𝐴 ∈ 𝑊) |
7 | | eqid 2622 |
. . . . 5
⊢ (𝑀 ↾s 𝐴) = (𝑀 ↾s 𝐴) |
8 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
9 | 1, 8 | mgpbas 18495 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑀) |
10 | 7, 9 | ressid2 15928 |
. . . 4
⊢
(((Base‘𝑅)
⊆ 𝐴 ∧ 𝑀 ∈ V ∧ 𝐴 ∈ 𝑊) → (𝑀 ↾s 𝐴) = 𝑀) |
11 | 2, 5, 6, 10 | syl3anc 1326 |
. . 3
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ (Base‘𝑅) ⊆ 𝐴) → (𝑀 ↾s 𝐴) = 𝑀) |
12 | | simpll 790 |
. . . . 5
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ (Base‘𝑅) ⊆ 𝐴) → 𝑅 ∈ 𝑉) |
13 | | mgpress.1 |
. . . . . 6
⊢ 𝑆 = (𝑅 ↾s 𝐴) |
14 | 13, 8 | ressid2 15928 |
. . . . 5
⊢
(((Base‘𝑅)
⊆ 𝐴 ∧ 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → 𝑆 = 𝑅) |
15 | 2, 12, 6, 14 | syl3anc 1326 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ (Base‘𝑅) ⊆ 𝐴) → 𝑆 = 𝑅) |
16 | 15 | fveq2d 6195 |
. . 3
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ (Base‘𝑅) ⊆ 𝐴) → (mulGrp‘𝑆) = (mulGrp‘𝑅)) |
17 | 1, 11, 16 | 3eqtr4a 2682 |
. 2
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ (Base‘𝑅) ⊆ 𝐴) → (𝑀 ↾s 𝐴) = (mulGrp‘𝑆)) |
18 | | eqid 2622 |
. . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) |
19 | 1, 18 | mgpval 18492 |
. . . 4
⊢ 𝑀 = (𝑅 sSet 〈(+g‘ndx),
(.r‘𝑅)〉) |
20 | 19 | oveq1i 6660 |
. . 3
⊢ (𝑀 sSet 〈(Base‘ndx),
(𝐴 ∩ (Base‘𝑅))〉) = ((𝑅 sSet 〈(+g‘ndx),
(.r‘𝑅)〉) sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉) |
21 | | simpr 477 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → ¬ (Base‘𝑅) ⊆ 𝐴) |
22 | 4 | a1i 11 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → 𝑀 ∈ V) |
23 | | simplr 792 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → 𝐴 ∈ 𝑊) |
24 | 7, 9 | ressval2 15929 |
. . . 4
⊢ ((¬
(Base‘𝑅) ⊆
𝐴 ∧ 𝑀 ∈ V ∧ 𝐴 ∈ 𝑊) → (𝑀 ↾s 𝐴) = (𝑀 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉)) |
25 | 21, 22, 23, 24 | syl3anc 1326 |
. . 3
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → (𝑀 ↾s 𝐴) = (𝑀 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉)) |
26 | | eqid 2622 |
. . . . . 6
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
27 | | eqid 2622 |
. . . . . 6
⊢
(.r‘𝑆) = (.r‘𝑆) |
28 | 26, 27 | mgpval 18492 |
. . . . 5
⊢
(mulGrp‘𝑆) =
(𝑆 sSet
〈(+g‘ndx), (.r‘𝑆)〉) |
29 | | simpll 790 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → 𝑅 ∈ 𝑉) |
30 | 13, 8 | ressval2 15929 |
. . . . . . 7
⊢ ((¬
(Base‘𝑅) ⊆
𝐴 ∧ 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → 𝑆 = (𝑅 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉)) |
31 | 21, 29, 23, 30 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → 𝑆 = (𝑅 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉)) |
32 | 13, 18 | ressmulr 16006 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑊 → (.r‘𝑅) = (.r‘𝑆)) |
33 | 32 | eqcomd 2628 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑊 → (.r‘𝑆) = (.r‘𝑅)) |
34 | 33 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → (.r‘𝑆) = (.r‘𝑅)) |
35 | 34 | opeq2d 4409 |
. . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → 〈(+g‘ndx),
(.r‘𝑆)〉 = 〈(+g‘ndx),
(.r‘𝑅)〉) |
36 | 31, 35 | oveq12d 6668 |
. . . . 5
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → (𝑆 sSet 〈(+g‘ndx),
(.r‘𝑆)〉) = ((𝑅 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉) sSet
〈(+g‘ndx), (.r‘𝑅)〉)) |
37 | 28, 36 | syl5eq 2668 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → (mulGrp‘𝑆) = ((𝑅 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉) sSet
〈(+g‘ndx), (.r‘𝑅)〉)) |
38 | | 1ne2 11240 |
. . . . . . 7
⊢ 1 ≠
2 |
39 | 38 | necomi 2848 |
. . . . . 6
⊢ 2 ≠
1 |
40 | | plusgndx 15976 |
. . . . . . 7
⊢
(+g‘ndx) = 2 |
41 | | basendx 15923 |
. . . . . . 7
⊢
(Base‘ndx) = 1 |
42 | 40, 41 | neeq12i 2860 |
. . . . . 6
⊢
((+g‘ndx) ≠ (Base‘ndx) ↔ 2 ≠
1) |
43 | 39, 42 | mpbir 221 |
. . . . 5
⊢
(+g‘ndx) ≠ (Base‘ndx) |
44 | | fvex 6201 |
. . . . . 6
⊢
(.r‘𝑅) ∈ V |
45 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝑅)
∈ V |
46 | 45 | inex2 4800 |
. . . . . 6
⊢ (𝐴 ∩ (Base‘𝑅)) ∈ V |
47 | | fvex 6201 |
. . . . . . 7
⊢
(+g‘ndx) ∈ V |
48 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘ndx) ∈ V |
49 | 47, 48 | setscom 15903 |
. . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ (+g‘ndx) ≠
(Base‘ndx)) ∧ ((.r‘𝑅) ∈ V ∧ (𝐴 ∩ (Base‘𝑅)) ∈ V)) → ((𝑅 sSet 〈(+g‘ndx),
(.r‘𝑅)〉) sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉) = ((𝑅 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉) sSet
〈(+g‘ndx), (.r‘𝑅)〉)) |
50 | 44, 46, 49 | mpanr12 721 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ (+g‘ndx) ≠
(Base‘ndx)) → ((𝑅 sSet 〈(+g‘ndx),
(.r‘𝑅)〉) sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉) = ((𝑅 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉) sSet
〈(+g‘ndx), (.r‘𝑅)〉)) |
51 | 29, 43, 50 | sylancl 694 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → ((𝑅 sSet 〈(+g‘ndx),
(.r‘𝑅)〉) sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉) = ((𝑅 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉) sSet
〈(+g‘ndx), (.r‘𝑅)〉)) |
52 | 37, 51 | eqtr4d 2659 |
. . 3
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → (mulGrp‘𝑆) = ((𝑅 sSet 〈(+g‘ndx),
(.r‘𝑅)〉) sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑅))〉)) |
53 | 20, 25, 52 | 3eqtr4a 2682 |
. 2
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ ¬ (Base‘𝑅) ⊆ 𝐴) → (𝑀 ↾s 𝐴) = (mulGrp‘𝑆)) |
54 | 17, 53 | pm2.61dan 832 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑀 ↾s 𝐴) = (mulGrp‘𝑆)) |