Metamath Proof Explorer

Theorem subrngpropd

Description: If two structures have the same ring components (properties), they have the same set of subrings. (Contributed by AV, 17-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 subrngpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 subrngpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 subrngpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4 subrngpropd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
5 1 2 3 4 rngpropd ⊢ ( 𝜑 → ( 𝐾 ∈ Rng ↔ 𝐿 ∈ Rng ) )
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 rngpropd ⊢ ( 𝜑 → ( ( 𝐾 ↾s 𝑠 ) ∈ Rng ↔ ( 𝐿 ↾s 𝑠 ) ∈ Rng ) )
42 1 2 eqtr3d ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
43 42 sseq2d ⊢ ( 𝜑 → ( 𝑠 ⊆ ( Base ‘ 𝐾 ) ↔ 𝑠 ⊆ ( Base ‘ 𝐿 ) ) )
44 5 41 43 3anbi123d ⊢ ( 𝜑 → ( ( 𝐾 ∈ Rng ∧ ( 𝐾 ↾s 𝑠 ) ∈ Rng ∧ 𝑠 ⊆ ( Base ‘ 𝐾 ) ) ↔ ( 𝐿 ∈ Rng ∧ ( 𝐿 ↾s 𝑠 ) ∈ Rng ∧ 𝑠 ⊆ ( Base ‘ 𝐿 ) ) ) )
45 8 issubrng ⊢ ( 𝑠 ∈ ( SubRng ‘ 𝐾 ) ↔ ( 𝐾 ∈ Rng ∧ ( 𝐾 ↾s 𝑠 ) ∈ Rng ∧ 𝑠 ⊆ ( Base ‘ 𝐾 ) ) )
46 14 issubrng ⊢ ( 𝑠 ∈ ( SubRng ‘ 𝐿 ) ↔ ( 𝐿 ∈ Rng ∧ ( 𝐿 ↾s 𝑠 ) ∈ Rng ∧ 𝑠 ⊆ ( Base ‘ 𝐿 ) ) )
47 44 45 46 3bitr4g ⊢ ( 𝜑 → ( 𝑠 ∈ ( SubRng ‘ 𝐾 ) ↔ 𝑠 ∈ ( SubRng ‘ 𝐿 ) ) )
48 47 eqrdv ⊢ ( 𝜑 → ( SubRng ‘ 𝐾 ) = ( SubRng ‘ 𝐿 ) )