Metamath Proof Explorer

Theorem rhmpropd

Description: Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses rhmpropd.a ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐽 ) )
rhmpropd.b ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝐾 ) )
rhmpropd.c ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
rhmpropd.d ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝑀 ) )
rhmpropd.e ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐽 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
rhmpropd.f ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
rhmpropd.g ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐽 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
rhmpropd.h ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑀 ) 𝑦 ) )
Assertion rhmpropd ( 𝜑 → ( 𝐽 RingHom 𝐾 ) = ( 𝐿 RingHom 𝑀 ) )

Proof

Step Hyp Ref Expression
1 rhmpropd.a ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐽 ) )
2 rhmpropd.b ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝐾 ) )
3 rhmpropd.c ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
4 rhmpropd.d ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝑀 ) )
5 rhmpropd.e ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐽 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
6 rhmpropd.f ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
7 rhmpropd.g ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐽 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
8 rhmpropd.h ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑀 ) 𝑦 ) )
9 1 3 5 7 ringpropd ⊢ ( 𝜑 → ( 𝐽 ∈ Ring ↔ 𝐿 ∈ Ring ) )
10 2 4 6 8 ringpropd ⊢ ( 𝜑 → ( 𝐾 ∈ Ring ↔ 𝑀 ∈ Ring ) )
11 9 10 anbi12d ⊢ ( 𝜑 → ( ( 𝐽 ∈ Ring ∧ 𝐾 ∈ Ring ) ↔ ( 𝐿 ∈ Ring ∧ 𝑀 ∈ Ring ) ) )
12 1 2 3 4 5 6 ghmpropd ⊢ ( 𝜑 → ( 𝐽 GrpHom 𝐾 ) = ( 𝐿 GrpHom 𝑀 ) )
13 12 eleq2d ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ↔ 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) ) )
14 eqid ⊢ ( mulGrp ‘ 𝐽 ) = ( mulGrp ‘ 𝐽 )
15 eqid ⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
16 14 15 mgpbas ⊢ ( Base ‘ 𝐽 ) = ( Base ‘ ( mulGrp ‘ 𝐽 ) )
17 1 16 eqtrdi ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( mulGrp ‘ 𝐽 ) ) )
18 eqid ⊢ ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
19 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
20 18 19 mgpbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
21 2 20 eqtrdi ⊢ ( 𝜑 → 𝐶 = ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
22 eqid ⊢ ( mulGrp ‘ 𝐿 ) = ( mulGrp ‘ 𝐿 )
23 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
24 22 23 mgpbas ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ ( mulGrp ‘ 𝐿 ) )
25 3 24 eqtrdi ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( mulGrp ‘ 𝐿 ) ) )
26 eqid ⊢ ( mulGrp ‘ 𝑀 ) = ( mulGrp ‘ 𝑀 )
27 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
28 26 27 mgpbas ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ ( mulGrp ‘ 𝑀 ) )
29 4 28 eqtrdi ⊢ ( 𝜑 → 𝐶 = ( Base ‘ ( mulGrp ‘ 𝑀 ) ) )
30 eqid ⊢ ( .r ‘ 𝐽 ) = ( .r ‘ 𝐽 )
31 14 30 mgpplusg ⊢ ( .r ‘ 𝐽 ) = ( +g ‘ ( mulGrp ‘ 𝐽 ) )
32 31 oveqi ⊢ ( 𝑥 ( .r ‘ 𝐽 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐽 ) ) 𝑦 )
33 eqid ⊢ ( .r ‘ 𝐿 ) = ( .r ‘ 𝐿 )
34 22 33 mgpplusg ⊢ ( .r ‘ 𝐿 ) = ( +g ‘ ( mulGrp ‘ 𝐿 ) )
35 34 oveqi ⊢ ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐿 ) ) 𝑦 )
36 7 32 35 3eqtr3g ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐽 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐿 ) ) 𝑦 ) )
37 eqid ⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
38 18 37 mgpplusg ⊢ ( .r ‘ 𝐾 ) = ( +g ‘ ( mulGrp ‘ 𝐾 ) )
39 38 oveqi ⊢ ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 )
40 eqid ⊢ ( .r ‘ 𝑀 ) = ( .r ‘ 𝑀 )
41 26 40 mgpplusg ⊢ ( .r ‘ 𝑀 ) = ( +g ‘ ( mulGrp ‘ 𝑀 ) )
42 41 oveqi ⊢ ( 𝑥 ( .r ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝑀 ) ) 𝑦 )
43 8 39 42 3eqtr3g ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝑀 ) ) 𝑦 ) )
44 17 21 25 29 36 43 mhmpropd ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝐽 ) MndHom ( mulGrp ‘ 𝐾 ) ) = ( ( mulGrp ‘ 𝐿 ) MndHom ( mulGrp ‘ 𝑀 ) ) )
45 44 eleq2d ⊢ ( 𝜑 → ( 𝑓 ∈ ( ( mulGrp ‘ 𝐽 ) MndHom ( mulGrp ‘ 𝐾 ) ) ↔ 𝑓 ∈ ( ( mulGrp ‘ 𝐿 ) MndHom ( mulGrp ‘ 𝑀 ) ) ) )
46 13 45 anbi12d ⊢ ( 𝜑 → ( ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝑓 ∈ ( ( mulGrp ‘ 𝐽 ) MndHom ( mulGrp ‘ 𝐾 ) ) ) ↔ ( 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) ∧ 𝑓 ∈ ( ( mulGrp ‘ 𝐿 ) MndHom ( mulGrp ‘ 𝑀 ) ) ) ) )
47 11 46 anbi12d ⊢ ( 𝜑 → ( ( ( 𝐽 ∈ Ring ∧ 𝐾 ∈ Ring ) ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝑓 ∈ ( ( mulGrp ‘ 𝐽 ) MndHom ( mulGrp ‘ 𝐾 ) ) ) ) ↔ ( ( 𝐿 ∈ Ring ∧ 𝑀 ∈ Ring ) ∧ ( 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) ∧ 𝑓 ∈ ( ( mulGrp ‘ 𝐿 ) MndHom ( mulGrp ‘ 𝑀 ) ) ) ) ) )
48 14 18 isrhm ⊢ ( 𝑓 ∈ ( 𝐽 RingHom 𝐾 ) ↔ ( ( 𝐽 ∈ Ring ∧ 𝐾 ∈ Ring ) ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝑓 ∈ ( ( mulGrp ‘ 𝐽 ) MndHom ( mulGrp ‘ 𝐾 ) ) ) ) )
49 22 26 isrhm ⊢ ( 𝑓 ∈ ( 𝐿 RingHom 𝑀 ) ↔ ( ( 𝐿 ∈ Ring ∧ 𝑀 ∈ Ring ) ∧ ( 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) ∧ 𝑓 ∈ ( ( mulGrp ‘ 𝐿 ) MndHom ( mulGrp ‘ 𝑀 ) ) ) ) )
50 47 48 49 3bitr4g ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐽 RingHom 𝐾 ) ↔ 𝑓 ∈ ( 𝐿 RingHom 𝑀 ) ) )
51 50 eqrdv ⊢ ( 𝜑 → ( 𝐽 RingHom 𝐾 ) = ( 𝐿 RingHom 𝑀 ) )