Metamath Proof Explorer

Theorem mgpress

Description: Subgroup commutes with the multiplicative group operator. (Contributed by Mario Carneiro, 10-Jan-2015) (Proof shortened by AV, 18-Oct-2024)

Ref Expression
Hypotheses mgpress.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
mgpress.2 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion mgpress ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑀 ↾s 𝐴 ) = ( mulGrp ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 mgpress.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2 mgpress.2 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
3 simpr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( Base ‘ 𝑅 ) ⊆ 𝐴 )
4 2 fvexi ⊢ 𝑀 ∈ V
5 4 a1i ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → 𝑀 ∈ V )
6 simplr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → 𝐴 ∈ 𝑊 )
7 eqid ⊢ ( 𝑀 ↾s 𝐴 ) = ( 𝑀 ↾s 𝐴 )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 2 8 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 )
10 7 9 ressid2 ⊢ ( ( ( Base ‘ 𝑅 ) ⊆ 𝐴 ∧ 𝑀 ∈ V ∧ 𝐴 ∈ 𝑊 ) → ( 𝑀 ↾s 𝐴 ) = 𝑀 )
11 3 5 6 10 syl3anc ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( 𝑀 ↾s 𝐴 ) = 𝑀 )
12 simpll ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → 𝑅 ∈ 𝑉 )
13 1 8 ressid2 ⊢ ( ( ( Base ‘ 𝑅 ) ⊆ 𝐴 ∧ 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → 𝑆 = 𝑅 )
14 3 12 6 13 syl3anc ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → 𝑆 = 𝑅 )
15 14 fveq2d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑅 ) )
16 2 11 15 3eqtr4a ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( 𝑀 ↾s 𝐴 ) = ( mulGrp ‘ 𝑆 ) )
17 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
18 2 17 mgpval ⊢ 𝑀 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ )
19 18 oveq1i ⊢ ( 𝑀 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) = ( ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ )
20 simpr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 )
21 4 a1i ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → 𝑀 ∈ V )
22 simplr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → 𝐴 ∈ 𝑊 )
23 7 9 ressval2 ⊢ ( ( ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ∧ 𝑀 ∈ V ∧ 𝐴 ∈ 𝑊 ) → ( 𝑀 ↾s 𝐴 ) = ( 𝑀 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) )
24 20 21 22 23 syl3anc ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( 𝑀 ↾s 𝐴 ) = ( 𝑀 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) )
25 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
26 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
27 25 26 mgpval ⊢ ( mulGrp ‘ 𝑆 ) = ( 𝑆 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑆 ) ⟩ )
28 simpll ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → 𝑅 ∈ 𝑉 )
29 1 8 ressval2 ⊢ ( ( ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ∧ 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → 𝑆 = ( 𝑅 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) )
30 20 28 22 29 syl3anc ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → 𝑆 = ( 𝑅 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) )
31 1 17 ressmulr ⊢ ( 𝐴 ∈ 𝑊 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
32 31 eqcomd ⊢ ( 𝐴 ∈ 𝑊 → ( .r ‘ 𝑆 ) = ( .r ‘ 𝑅 ) )
33 32 ad2antlr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( .r ‘ 𝑆 ) = ( .r ‘ 𝑅 ) )
34 33 opeq2d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑆 ) ⟩ = ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ )
35 30 34 oveq12d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( 𝑆 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑆 ) ⟩ ) = ( ( 𝑅 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ ) )
36 27 35 eqtrid ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( mulGrp ‘ 𝑆 ) = ( ( 𝑅 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ ) )
37 basendxnplusgndx ⊢ ( Base ‘ ndx ) ≠ ( +g ‘ ndx )
38 37 necomi ⊢ ( +g ‘ ndx ) ≠ ( Base ‘ ndx )
39 fvex ⊢ ( .r ‘ 𝑅 ) ∈ V
40 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
41 40 inex2 ⊢ ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ∈ V
42 fvex ⊢ ( +g ‘ ndx ) ∈ V
43 fvex ⊢ ( Base ‘ ndx ) ∈ V
44 42 43 setscom ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ ( +g ‘ ndx ) ≠ ( Base ‘ ndx ) ) ∧ ( ( .r ‘ 𝑅 ) ∈ V ∧ ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ∈ V ) ) → ( ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) = ( ( 𝑅 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ ) )
45 39 41 44 mpanr12 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( +g ‘ ndx ) ≠ ( Base ‘ ndx ) ) → ( ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) = ( ( 𝑅 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ ) )
46 28 38 45 sylancl ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) = ( ( 𝑅 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ ) )
47 36 46 eqtr4d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( mulGrp ‘ 𝑆 ) = ( ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) )
48 19 24 47 3eqtr4a ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( 𝑀 ↾s 𝐴 ) = ( mulGrp ‘ 𝑆 ) )
49 16 48 pm2.61dan ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑀 ↾s 𝐴 ) = ( mulGrp ‘ 𝑆 ) )