Metamath Proof Explorer

Theorem prdsmgp

Description: The multiplicative monoid of a product is the product of the multiplicative monoids of the factors. (Contributed by Mario Carneiro, 11-Mar-2015)

Ref Expression
Hypotheses prdsmgp.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdsmgp.m ⊢ 𝑀 = ( mulGrp ‘ 𝑌 )
prdsmgp.z ⊢ 𝑍 = ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) )
prdsmgp.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
prdsmgp.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
prdsmgp.r ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
Assertion prdsmgp ( 𝜑 → ( ( Base ‘ 𝑀 ) = ( Base ‘ 𝑍 ) ∧ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 prdsmgp.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsmgp.m ⊢ 𝑀 = ( mulGrp ‘ 𝑌 )
3 prdsmgp.z ⊢ 𝑍 = ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) )
4 prdsmgp.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5 prdsmgp.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
6 prdsmgp.r ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
7 eqid ⊢ ( mulGrp ‘ ( 𝑅 ‘ 𝑥 ) ) = ( mulGrp ‘ ( 𝑅 ‘ 𝑥 ) )
8 eqid ⊢ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑥 ) )
9 7 8 mgpbas ⊢ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) = ( Base ‘ ( mulGrp ‘ ( 𝑅 ‘ 𝑥 ) ) )
10 fvco2 ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝑥 ∈ 𝐼 ) → ( ( mulGrp ∘ 𝑅 ) ‘ 𝑥 ) = ( mulGrp ‘ ( 𝑅 ‘ 𝑥 ) ) )
11 6 10 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( mulGrp ∘ 𝑅 ) ‘ 𝑥 ) = ( mulGrp ‘ ( 𝑅 ‘ 𝑥 ) ) )
12 11 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( mulGrp ‘ ( 𝑅 ‘ 𝑥 ) ) = ( ( mulGrp ∘ 𝑅 ) ‘ 𝑥 ) )
13 12 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( mulGrp ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( Base ‘ ( ( mulGrp ∘ 𝑅 ) ‘ 𝑥 ) ) )
14 9 13 syl5eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) = ( Base ‘ ( ( mulGrp ∘ 𝑅 ) ‘ 𝑥 ) ) )
15 14 ixpeq2dva ⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( ( mulGrp ∘ 𝑅 ) ‘ 𝑥 ) ) )
16 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
17 2 16 mgpbas ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑀 )
18 17 eqcomi ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑌 )
19 1 18 5 4 6 prdsbas2 ⊢ ( 𝜑 → ( Base ‘ 𝑀 ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
20 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
21 fnmgp ⊢ mulGrp Fn V
22 ssv ⊢ ran 𝑅 ⊆ V
23 22 a1i ⊢ ( 𝜑 → ran 𝑅 ⊆ V )
24 fnco ⊢ ( ( mulGrp Fn V ∧ 𝑅 Fn 𝐼 ∧ ran 𝑅 ⊆ V ) → ( mulGrp ∘ 𝑅 ) Fn 𝐼 )
25 21 6 23 24 mp3an2i ⊢ ( 𝜑 → ( mulGrp ∘ 𝑅 ) Fn 𝐼 )
26 3 20 5 4 25 prdsbas2 ⊢ ( 𝜑 → ( Base ‘ 𝑍 ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( ( mulGrp ∘ 𝑅 ) ‘ 𝑥 ) ) )
27 15 19 26 3eqtr4d ⊢ ( 𝜑 → ( Base ‘ 𝑀 ) = ( Base ‘ 𝑍 ) )
28 eqid ⊢ ( .r ‘ 𝑌 ) = ( .r ‘ 𝑌 )
29 2 28 mgpplusg ⊢ ( .r ‘ 𝑌 ) = ( +g ‘ 𝑀 )
30 eqid ⊢ ( mulGrp ‘ ( 𝑅 ‘ 𝑧 ) ) = ( mulGrp ‘ ( 𝑅 ‘ 𝑧 ) )
31 eqid ⊢ ( .r ‘ ( 𝑅 ‘ 𝑧 ) ) = ( .r ‘ ( 𝑅 ‘ 𝑧 ) )
32 30 31 mgpplusg ⊢ ( .r ‘ ( 𝑅 ‘ 𝑧 ) ) = ( +g ‘ ( mulGrp ‘ ( 𝑅 ‘ 𝑧 ) ) )
33 fvco2 ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( ( mulGrp ∘ 𝑅 ) ‘ 𝑧 ) = ( mulGrp ‘ ( 𝑅 ‘ 𝑧 ) ) )
34 6 33 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( ( mulGrp ∘ 𝑅 ) ‘ 𝑧 ) = ( mulGrp ‘ ( 𝑅 ‘ 𝑧 ) ) )
35 34 eqcomd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( mulGrp ‘ ( 𝑅 ‘ 𝑧 ) ) = ( ( mulGrp ∘ 𝑅 ) ‘ 𝑧 ) )
36 35 fveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( +g ‘ ( mulGrp ‘ ( 𝑅 ‘ 𝑧 ) ) ) = ( +g ‘ ( ( mulGrp ∘ 𝑅 ) ‘ 𝑧 ) ) )
37 32 36 syl5eq ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( .r ‘ ( 𝑅 ‘ 𝑧 ) ) = ( +g ‘ ( ( mulGrp ∘ 𝑅 ) ‘ 𝑧 ) ) )
38 37 oveqd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑧 ) ( .r ‘ ( 𝑅 ‘ 𝑧 ) ) ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ ( ( mulGrp ∘ 𝑅 ) ‘ 𝑧 ) ) ( 𝑦 ‘ 𝑧 ) ) )
39 38 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑧 ) ( .r ‘ ( 𝑅 ‘ 𝑧 ) ) ( 𝑦 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ ( ( mulGrp ∘ 𝑅 ) ‘ 𝑧 ) ) ( 𝑦 ‘ 𝑧 ) ) ) )
40 27 27 39 mpoeq123dv ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑀 ) , 𝑦 ∈ ( Base ‘ 𝑀 ) ↦ ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑧 ) ( .r ‘ ( 𝑅 ‘ 𝑧 ) ) ( 𝑦 ‘ 𝑧 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝑍 ) , 𝑦 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ ( ( mulGrp ∘ 𝑅 ) ‘ 𝑧 ) ) ( 𝑦 ‘ 𝑧 ) ) ) ) )
41 fnex ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) → 𝑅 ∈ V )
42 6 4 41 syl2anc ⊢ ( 𝜑 → 𝑅 ∈ V )
43 6 fndmd ⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
44 1 5 42 18 43 28 prdsmulr ⊢ ( 𝜑 → ( .r ‘ 𝑌 ) = ( 𝑥 ∈ ( Base ‘ 𝑀 ) , 𝑦 ∈ ( Base ‘ 𝑀 ) ↦ ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑧 ) ( .r ‘ ( 𝑅 ‘ 𝑧 ) ) ( 𝑦 ‘ 𝑧 ) ) ) ) )
45 fnex ⊢ ( ( ( mulGrp ∘ 𝑅 ) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) → ( mulGrp ∘ 𝑅 ) ∈ V )
46 25 4 45 syl2anc ⊢ ( 𝜑 → ( mulGrp ∘ 𝑅 ) ∈ V )
47 25 fndmd ⊢ ( 𝜑 → dom ( mulGrp ∘ 𝑅 ) = 𝐼 )
48 eqid ⊢ ( +g ‘ 𝑍 ) = ( +g ‘ 𝑍 )
49 3 5 46 20 47 48 prdsplusg ⊢ ( 𝜑 → ( +g ‘ 𝑍 ) = ( 𝑥 ∈ ( Base ‘ 𝑍 ) , 𝑦 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ ( ( mulGrp ∘ 𝑅 ) ‘ 𝑧 ) ) ( 𝑦 ‘ 𝑧 ) ) ) ) )
50 40 44 49 3eqtr4d ⊢ ( 𝜑 → ( .r ‘ 𝑌 ) = ( +g ‘ 𝑍 ) )
51 29 50 eqtr3id ⊢ ( 𝜑 → ( +g ‘ 𝑀 ) = ( +g ‘ 𝑍 ) )
52 27 51 jca ⊢ ( 𝜑 → ( ( Base ‘ 𝑀 ) = ( Base ‘ 𝑍 ) ∧ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑍 ) ) )