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 
|- ( ph -> B = ( Base ` K ) )
lidlpropd.2 
|- ( ph -> B = ( Base ` L ) )
lidlpropd.3 
|- ( ph -> B C_ W )
lidlpropd.4 
|- ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
lidlpropd.5 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) e. W )
lidlpropd.6 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
Assertion lidlrsppropd 
|- ( ph -> ( ( LIdeal ` K ) = ( LIdeal ` L ) /\ ( RSpan ` K ) = ( RSpan ` L ) ) )

Proof

Step Hyp Ref Expression
1 lidlpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 lidlpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 lidlpropd.3 
 |-  ( ph -> B C_ W )
4 lidlpropd.4 
 |-  ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
5 lidlpropd.5 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) e. W )
6 lidlpropd.6 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
7 rlmbas 
 |-  ( Base ` K ) = ( Base ` ( ringLMod ` K ) )
8 1 7 eqtrdi 
 |-  ( ph -> B = ( Base ` ( ringLMod ` K ) ) )
9 rlmbas 
 |-  ( Base ` L ) = ( Base ` ( ringLMod ` L ) )
10 2 9 eqtrdi 
 |-  ( ph -> B = ( Base ` ( ringLMod ` L ) ) )
11 rlmplusg 
 |-  ( +g ` K ) = ( +g ` ( ringLMod ` K ) )
12 11 oveqi 
 |-  ( x ( +g ` K ) y ) = ( x ( +g ` ( ringLMod ` K ) ) y )
13 rlmplusg 
 |-  ( +g ` L ) = ( +g ` ( ringLMod ` L ) )
14 13 oveqi 
 |-  ( x ( +g ` L ) y ) = ( x ( +g ` ( ringLMod ` L ) ) y )
15 4 12 14 3eqtr3g 
 |-  ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` ( ringLMod ` K ) ) y ) = ( x ( +g ` ( ringLMod ` L ) ) y ) )
16 rlmvsca 
 |-  ( .r ` K ) = ( .s ` ( ringLMod ` K ) )
17 16 oveqi 
 |-  ( x ( .r ` K ) y ) = ( x ( .s ` ( ringLMod ` K ) ) y )
18 17 5 eqeltrrid 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .s ` ( ringLMod ` K ) ) y ) e. W )
19 rlmvsca 
 |-  ( .r ` L ) = ( .s ` ( ringLMod ` L ) )
20 19 oveqi 
 |-  ( x ( .r ` L ) y ) = ( x ( .s ` ( ringLMod ` L ) ) y )
21 6 17 20 3eqtr3g 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .s ` ( ringLMod ` K ) ) y ) = ( x ( .s ` ( ringLMod ` L ) ) y ) )
22 baseid 
 |-  Base = Slot ( Base ` ndx )
23 eqid 
 |-  ( Base ` K ) = ( Base ` K )
24 22 23 strfvi 
 |-  ( Base ` K ) = ( Base ` ( _I ` K ) )
25 rlmsca2 
 |-  ( _I ` K ) = ( Scalar ` ( ringLMod ` K ) )
26 25 fveq2i 
 |-  ( Base ` ( _I ` K ) ) = ( Base ` ( Scalar ` ( ringLMod ` K ) ) )
27 24 26 eqtri 
 |-  ( Base ` K ) = ( Base ` ( Scalar ` ( ringLMod ` K ) ) )
28 1 27 eqtrdi 
 |-  ( ph -> B = ( Base ` ( Scalar ` ( ringLMod ` K ) ) ) )
29 eqid 
 |-  ( Base ` L ) = ( Base ` L )
30 22 29 strfvi 
 |-  ( Base ` L ) = ( Base ` ( _I ` L ) )
31 rlmsca2 
 |-  ( _I ` L ) = ( Scalar ` ( ringLMod ` L ) )
32 31 fveq2i 
 |-  ( Base ` ( _I ` L ) ) = ( Base ` ( Scalar ` ( ringLMod ` L ) ) )
33 30 32 eqtri 
 |-  ( Base ` L ) = ( Base ` ( Scalar ` ( ringLMod ` L ) ) )
34 2 33 eqtrdi 
 |-  ( ph -> B = ( Base ` ( Scalar ` ( ringLMod ` L ) ) ) )
35 8 10 3 15 18 21 28 34 lsspropd 
 |-  ( ph -> ( LSubSp ` ( ringLMod ` K ) ) = ( LSubSp ` ( ringLMod ` L ) ) )
36 lidlval 
 |-  ( LIdeal ` K ) = ( LSubSp ` ( ringLMod ` K ) )
37 lidlval 
 |-  ( LIdeal ` L ) = ( LSubSp ` ( ringLMod ` L ) )
38 35 36 37 3eqtr4g 
 |-  ( ph -> ( LIdeal ` K ) = ( LIdeal ` L ) )
39 fvexd 
 |-  ( ph -> ( ringLMod ` K ) e. _V )
40 fvexd 
 |-  ( ph -> ( ringLMod ` L ) e. _V )
41 8 10 3 15 18 21 28 34 39 40 lsppropd 
 |-  ( ph -> ( LSpan ` ( ringLMod ` K ) ) = ( LSpan ` ( ringLMod ` L ) ) )
42 rspval 
 |-  ( RSpan ` K ) = ( LSpan ` ( ringLMod ` K ) )
43 rspval 
 |-  ( RSpan ` L ) = ( LSpan ` ( ringLMod ` L ) )
44 41 42 43 3eqtr4g 
 |-  ( ph -> ( RSpan ` K ) = ( RSpan ` L ) )
45 38 44 jca 
 |-  ( ph -> ( ( LIdeal ` K ) = ( LIdeal ` L ) /\ ( RSpan ` K ) = ( RSpan ` L ) ) )