Metamath Proof Explorer

Theorem lidlrsppropd

Description: The left ideals and ring span of a ring depend only on the ring components. Here W is expected to be either B (when closure is available) or _V (when strong equality is available). (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses lidlpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
lidlpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
lidlpropd.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑊 )
lidlpropd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
lidlpropd.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) ∈ 𝑊 )
lidlpropd.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
Assertion lidlrsppropd ( 𝜑 → ( ( LIdeal ‘ 𝐾 ) = ( LIdeal ‘ 𝐿 ) ∧ ( RSpan ‘ 𝐾 ) = ( RSpan ‘ 𝐿 ) ) )

Proof

Step Hyp Ref Expression
1 lidlpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 lidlpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 lidlpropd.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑊 )
4 lidlpropd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
5 lidlpropd.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) ∈ 𝑊 )
6 lidlpropd.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
7 rlmbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( ringLMod ‘ 𝐾 ) )
8 1 7 eqtrdi ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( ringLMod ‘ 𝐾 ) ) )
9 rlmbas ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ ( ringLMod ‘ 𝐿 ) )
10 2 9 eqtrdi ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( ringLMod ‘ 𝐿 ) ) )
11 rlmplusg ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ ( ringLMod ‘ 𝐾 ) )
12 11 oveqi ⊢ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( ringLMod ‘ 𝐾 ) ) 𝑦 )
13 rlmplusg ⊢ ( +g ‘ 𝐿 ) = ( +g ‘ ( ringLMod ‘ 𝐿 ) )
14 13 oveqi ⊢ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( ringLMod ‘ 𝐿 ) ) 𝑦 )
15 4 12 14 3eqtr3g ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑥 ( +g ‘ ( ringLMod ‘ 𝐾 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( ringLMod ‘ 𝐿 ) ) 𝑦 ) )
16 rlmvsca ⊢ ( .r ‘ 𝐾 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝐾 ) )
17 16 oveqi ⊢ ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ ( ringLMod ‘ 𝐾 ) ) 𝑦 )
18 17 5 eqeltrrid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ ( ringLMod ‘ 𝐾 ) ) 𝑦 ) ∈ 𝑊 )
19 rlmvsca ⊢ ( .r ‘ 𝐿 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝐿 ) )
20 19 oveqi ⊢ ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ ( ringLMod ‘ 𝐿 ) ) 𝑦 )
21 6 17 20 3eqtr3g ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ ( ringLMod ‘ 𝐾 ) ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ ( ringLMod ‘ 𝐿 ) ) 𝑦 ) )
22 baseid ⊢ Base = Slot ( Base ‘ ndx )
23 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24 22 23 strfvi ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( I ‘ 𝐾 ) )
25 rlmsca2 ⊢ ( I ‘ 𝐾 ) = ( Scalar ‘ ( ringLMod ‘ 𝐾 ) )
26 25 fveq2i ⊢ ( Base ‘ ( I ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝐾 ) ) )
27 24 26 eqtri ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝐾 ) ) )
28 1 27 eqtrdi ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝐾 ) ) ) )
29 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
30 22 29 strfvi ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ ( I ‘ 𝐿 ) )
31 rlmsca2 ⊢ ( I ‘ 𝐿 ) = ( Scalar ‘ ( ringLMod ‘ 𝐿 ) )
32 31 fveq2i ⊢ ( Base ‘ ( I ‘ 𝐿 ) ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝐿 ) ) )
33 30 32 eqtri ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝐿 ) ) )
34 2 33 eqtrdi ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝐿 ) ) ) )
35 8 10 3 15 18 21 28 34 lsspropd ⊢ ( 𝜑 → ( LSubSp ‘ ( ringLMod ‘ 𝐾 ) ) = ( LSubSp ‘ ( ringLMod ‘ 𝐿 ) ) )
36 lidlval ⊢ ( LIdeal ‘ 𝐾 ) = ( LSubSp ‘ ( ringLMod ‘ 𝐾 ) )
37 lidlval ⊢ ( LIdeal ‘ 𝐿 ) = ( LSubSp ‘ ( ringLMod ‘ 𝐿 ) )
38 35 36 37 3eqtr4g ⊢ ( 𝜑 → ( LIdeal ‘ 𝐾 ) = ( LIdeal ‘ 𝐿 ) )
39 fvexd ⊢ ( 𝜑 → ( ringLMod ‘ 𝐾 ) ∈ V )
40 fvexd ⊢ ( 𝜑 → ( ringLMod ‘ 𝐿 ) ∈ V )
41 8 10 3 15 18 21 28 34 39 40 lsppropd ⊢ ( 𝜑 → ( LSpan ‘ ( ringLMod ‘ 𝐾 ) ) = ( LSpan ‘ ( ringLMod ‘ 𝐿 ) ) )
42 rspval ⊢ ( RSpan ‘ 𝐾 ) = ( LSpan ‘ ( ringLMod ‘ 𝐾 ) )
43 rspval ⊢ ( RSpan ‘ 𝐿 ) = ( LSpan ‘ ( ringLMod ‘ 𝐿 ) )
44 41 42 43 3eqtr4g ⊢ ( 𝜑 → ( RSpan ‘ 𝐾 ) = ( RSpan ‘ 𝐿 ) )
45 38 44 jca ⊢ ( 𝜑 → ( ( LIdeal ‘ 𝐾 ) = ( LIdeal ‘ 𝐿 ) ∧ ( RSpan ‘ 𝐾 ) = ( RSpan ‘ 𝐿 ) ) )