Metamath Proof Explorer


Theorem subrgpropd

Description: If two structures have the same group components (properties), they have the same set of subrings. (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypotheses subrgpropd.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
subrgpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
subrgpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
subrgpropd.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
Assertion subrgpropd ( 𝜑 → ( SubRing ‘ 𝐾 ) = ( SubRing ‘ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 subrgpropd.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
2 subrgpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
3 subrgpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
4 subrgpropd.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
5 1 2 3 4 ringpropd ( 𝜑 → ( 𝐾 ∈ Ring ↔ 𝐿 ∈ Ring ) )
6 1 ineq2d ( 𝜑 → ( 𝑠𝐵 ) = ( 𝑠 ∩ ( Base ‘ 𝐾 ) ) )
7 eqid ( 𝐾s 𝑠 ) = ( 𝐾s 𝑠 )
8 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 7 8 ressbas ( 𝑠 ∈ V → ( 𝑠 ∩ ( Base ‘ 𝐾 ) ) = ( Base ‘ ( 𝐾s 𝑠 ) ) )
10 9 elv ( 𝑠 ∩ ( Base ‘ 𝐾 ) ) = ( Base ‘ ( 𝐾s 𝑠 ) )
11 6 10 eqtrdi ( 𝜑 → ( 𝑠𝐵 ) = ( Base ‘ ( 𝐾s 𝑠 ) ) )
12 2 ineq2d ( 𝜑 → ( 𝑠𝐵 ) = ( 𝑠 ∩ ( Base ‘ 𝐿 ) ) )
13 eqid ( 𝐿s 𝑠 ) = ( 𝐿s 𝑠 )
14 eqid ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
15 13 14 ressbas ( 𝑠 ∈ V → ( 𝑠 ∩ ( Base ‘ 𝐿 ) ) = ( Base ‘ ( 𝐿s 𝑠 ) ) )
16 15 elv ( 𝑠 ∩ ( Base ‘ 𝐿 ) ) = ( Base ‘ ( 𝐿s 𝑠 ) )
17 12 16 eqtrdi ( 𝜑 → ( 𝑠𝐵 ) = ( Base ‘ ( 𝐿s 𝑠 ) ) )
18 elinel2 ( 𝑥 ∈ ( 𝑠𝐵 ) → 𝑥𝐵 )
19 elinel2 ( 𝑦 ∈ ( 𝑠𝐵 ) → 𝑦𝐵 )
20 18 19 anim12i ( ( 𝑥 ∈ ( 𝑠𝐵 ) ∧ 𝑦 ∈ ( 𝑠𝐵 ) ) → ( 𝑥𝐵𝑦𝐵 ) )
21 eqid ( +g𝐾 ) = ( +g𝐾 )
22 7 21 ressplusg ( 𝑠 ∈ V → ( +g𝐾 ) = ( +g ‘ ( 𝐾s 𝑠 ) ) )
23 22 elv ( +g𝐾 ) = ( +g ‘ ( 𝐾s 𝑠 ) )
24 23 oveqi ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝐾s 𝑠 ) ) 𝑦 )
25 eqid ( +g𝐿 ) = ( +g𝐿 )
26 13 25 ressplusg ( 𝑠 ∈ V → ( +g𝐿 ) = ( +g ‘ ( 𝐿s 𝑠 ) ) )
27 26 elv ( +g𝐿 ) = ( +g ‘ ( 𝐿s 𝑠 ) )
28 27 oveqi ( 𝑥 ( +g𝐿 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝐿s 𝑠 ) ) 𝑦 )
29 3 24 28 3eqtr3g ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g ‘ ( 𝐾s 𝑠 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝐿s 𝑠 ) ) 𝑦 ) )
30 20 29 sylan2 ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑠𝐵 ) ∧ 𝑦 ∈ ( 𝑠𝐵 ) ) ) → ( 𝑥 ( +g ‘ ( 𝐾s 𝑠 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝐿s 𝑠 ) ) 𝑦 ) )
31 eqid ( .r𝐾 ) = ( .r𝐾 )
32 7 31 ressmulr ( 𝑠 ∈ V → ( .r𝐾 ) = ( .r ‘ ( 𝐾s 𝑠 ) ) )
33 32 elv ( .r𝐾 ) = ( .r ‘ ( 𝐾s 𝑠 ) )
34 33 oveqi ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝐾s 𝑠 ) ) 𝑦 )
35 eqid ( .r𝐿 ) = ( .r𝐿 )
36 13 35 ressmulr ( 𝑠 ∈ V → ( .r𝐿 ) = ( .r ‘ ( 𝐿s 𝑠 ) ) )
37 36 elv ( .r𝐿 ) = ( .r ‘ ( 𝐿s 𝑠 ) )
38 37 oveqi ( 𝑥 ( .r𝐿 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝐿s 𝑠 ) ) 𝑦 )
39 4 34 38 3eqtr3g ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r ‘ ( 𝐾s 𝑠 ) ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝐿s 𝑠 ) ) 𝑦 ) )
40 20 39 sylan2 ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑠𝐵 ) ∧ 𝑦 ∈ ( 𝑠𝐵 ) ) ) → ( 𝑥 ( .r ‘ ( 𝐾s 𝑠 ) ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝐿s 𝑠 ) ) 𝑦 ) )
41 11 17 30 40 ringpropd ( 𝜑 → ( ( 𝐾s 𝑠 ) ∈ Ring ↔ ( 𝐿s 𝑠 ) ∈ Ring ) )
42 5 41 anbi12d ( 𝜑 → ( ( 𝐾 ∈ Ring ∧ ( 𝐾s 𝑠 ) ∈ Ring ) ↔ ( 𝐿 ∈ Ring ∧ ( 𝐿s 𝑠 ) ∈ Ring ) ) )
43 1 2 eqtr3d ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
44 43 sseq2d ( 𝜑 → ( 𝑠 ⊆ ( Base ‘ 𝐾 ) ↔ 𝑠 ⊆ ( Base ‘ 𝐿 ) ) )
45 1 2 4 rngidpropd ( 𝜑 → ( 1r𝐾 ) = ( 1r𝐿 ) )
46 45 eleq1d ( 𝜑 → ( ( 1r𝐾 ) ∈ 𝑠 ↔ ( 1r𝐿 ) ∈ 𝑠 ) )
47 44 46 anbi12d ( 𝜑 → ( ( 𝑠 ⊆ ( Base ‘ 𝐾 ) ∧ ( 1r𝐾 ) ∈ 𝑠 ) ↔ ( 𝑠 ⊆ ( Base ‘ 𝐿 ) ∧ ( 1r𝐿 ) ∈ 𝑠 ) ) )
48 42 47 anbi12d ( 𝜑 → ( ( ( 𝐾 ∈ Ring ∧ ( 𝐾s 𝑠 ) ∈ Ring ) ∧ ( 𝑠 ⊆ ( Base ‘ 𝐾 ) ∧ ( 1r𝐾 ) ∈ 𝑠 ) ) ↔ ( ( 𝐿 ∈ Ring ∧ ( 𝐿s 𝑠 ) ∈ Ring ) ∧ ( 𝑠 ⊆ ( Base ‘ 𝐿 ) ∧ ( 1r𝐿 ) ∈ 𝑠 ) ) ) )
49 eqid ( 1r𝐾 ) = ( 1r𝐾 )
50 8 49 issubrg ( 𝑠 ∈ ( SubRing ‘ 𝐾 ) ↔ ( ( 𝐾 ∈ Ring ∧ ( 𝐾s 𝑠 ) ∈ Ring ) ∧ ( 𝑠 ⊆ ( Base ‘ 𝐾 ) ∧ ( 1r𝐾 ) ∈ 𝑠 ) ) )
51 eqid ( 1r𝐿 ) = ( 1r𝐿 )
52 14 51 issubrg ( 𝑠 ∈ ( SubRing ‘ 𝐿 ) ↔ ( ( 𝐿 ∈ Ring ∧ ( 𝐿s 𝑠 ) ∈ Ring ) ∧ ( 𝑠 ⊆ ( Base ‘ 𝐿 ) ∧ ( 1r𝐿 ) ∈ 𝑠 ) ) )
53 48 50 52 3bitr4g ( 𝜑 → ( 𝑠 ∈ ( SubRing ‘ 𝐾 ) ↔ 𝑠 ∈ ( SubRing ‘ 𝐿 ) ) )
54 53 eqrdv ( 𝜑 → ( SubRing ‘ 𝐾 ) = ( SubRing ‘ 𝐿 ) )