This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐿 ) )