Metamath Proof Explorer


Theorem mgpressOLD

Description: Obsolete version of mgpress as of 18-Oct-2024. Subgroup commutes with the multiplication group operator. (Contributed by Mario Carneiro, 10-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses mgpress.1 𝑆 = ( 𝑅s 𝐴 )
mgpress.2 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion mgpressOLD ( ( 𝑅𝑉𝐴𝑊 ) → ( 𝑀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 1ne2 1 ≠ 2
38 37 necomi 2 ≠ 1
39 plusgndx ( +g ‘ ndx ) = 2
40 basendx ( Base ‘ ndx ) = 1
41 39 40 neeq12i ( ( +g ‘ ndx ) ≠ ( Base ‘ ndx ) ↔ 2 ≠ 1 )
42 38 41 mpbir ( +g ‘ ndx ) ≠ ( Base ‘ ndx )
43 fvex ( .r𝑅 ) ∈ V
44 fvex ( Base ‘ 𝑅 ) ∈ V
45 44 inex2 ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ∈ V
46 fvex ( +g ‘ ndx ) ∈ V
47 fvex ( Base ‘ ndx ) ∈ V
48 46 47 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𝑅 ) ⟩ ) )
49 43 45 48 mpanr12 ( ( 𝑅𝑉 ∧ ( +g ‘ ndx ) ≠ ( Base ‘ ndx ) ) → ( ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , ( .r𝑅 ) ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) = ( ( 𝑅 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) sSet ⟨ ( +g ‘ ndx ) , ( .r𝑅 ) ⟩ ) )
50 28 42 49 sylancl ( ( ( 𝑅𝑉𝐴𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , ( .r𝑅 ) ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) = ( ( 𝑅 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) sSet ⟨ ( +g ‘ ndx ) , ( .r𝑅 ) ⟩ ) )
51 36 50 eqtr4d ( ( ( 𝑅𝑉𝐴𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( mulGrp ‘ 𝑆 ) = ( ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , ( .r𝑅 ) ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑅 ) ) ⟩ ) )
52 19 24 51 3eqtr4a ( ( ( 𝑅𝑉𝐴𝑊 ) ∧ ¬ ( Base ‘ 𝑅 ) ⊆ 𝐴 ) → ( 𝑀s 𝐴 ) = ( mulGrp ‘ 𝑆 ) )
53 16 52 pm2.61dan ( ( 𝑅𝑉𝐴𝑊 ) → ( 𝑀s 𝐴 ) = ( mulGrp ‘ 𝑆 ) )