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

Metamath Proof Explorer

Theorem resssra

Description: The subring algebra of a restricted structure is the restriction of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses resssra.a 
|- A = ( Base ` R )
resssra.s 
|- S = ( R |`s B )
resssra.b 
|- ( ph -> B C_ A )
resssra.c 
|- ( ph -> C C_ B )
resssra.r 
|- ( ph -> R e. V )
Assertion resssra 
|- ( ph -> ( ( subringAlg ` S ) ` C ) = ( ( ( subringAlg ` R ) ` C ) |`s B ) )

Proof

Step Hyp Ref Expression
1 resssra.a 
 |-  A = ( Base ` R )
2 resssra.s 
 |-  S = ( R |`s B )
3 resssra.b 
 |-  ( ph -> B C_ A )
4 resssra.c 
 |-  ( ph -> C C_ B )
5 resssra.r 
 |-  ( ph -> R e. V )
6 eqidd 
 |-  ( ph -> ( ( subringAlg ` R ) ` C ) = ( ( subringAlg ` R ) ` C ) )
7 4 3 sstrd 
 |-  ( ph -> C C_ A )
8 7 1 sseqtrdi 
 |-  ( ph -> C C_ ( Base ` R ) )
9 6 8 srabase 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( ( subringAlg ` R ) ` C ) ) )
10 1 9 eqtrid 
 |-  ( ph -> A = ( Base ` ( ( subringAlg ` R ) ` C ) ) )
11 10 oveq2d 
 |-  ( ph -> ( ( ( subringAlg ` R ) ` C ) |`s A ) = ( ( ( subringAlg ` R ) ` C ) |`s ( Base ` ( ( subringAlg ` R ) ` C ) ) ) )
12 11 adantr 
 |-  ( ( ph /\ A C_ B ) -> ( ( ( subringAlg ` R ) ` C ) |`s A ) = ( ( ( subringAlg ` R ) ` C ) |`s ( Base ` ( ( subringAlg ` R ) ` C ) ) ) )
13 simpr 
 |-  ( ( ph /\ A C_ B ) -> A C_ B )
14 3 adantr 
 |-  ( ( ph /\ A C_ B ) -> B C_ A )
15 13 14 eqssd 
 |-  ( ( ph /\ A C_ B ) -> A = B )
16 15 oveq2d 
 |-  ( ( ph /\ A C_ B ) -> ( ( ( subringAlg ` R ) ` C ) |`s A ) = ( ( ( subringAlg ` R ) ` C ) |`s B ) )
17 fvex 
 |-  ( ( subringAlg ` R ) ` C ) e. _V
18 eqid 
 |-  ( Base ` ( ( subringAlg ` R ) ` C ) ) = ( Base ` ( ( subringAlg ` R ) ` C ) )
19 18 ressid 
 |-  ( ( ( subringAlg ` R ) ` C ) e. _V -> ( ( ( subringAlg ` R ) ` C ) |`s ( Base ` ( ( subringAlg ` R ) ` C ) ) ) = ( ( subringAlg ` R ) ` C ) )
20 17 19 mp1i 
 |-  ( ( ph /\ A C_ B ) -> ( ( ( subringAlg ` R ) ` C ) |`s ( Base ` ( ( subringAlg ` R ) ` C ) ) ) = ( ( subringAlg ` R ) ` C ) )
21 12 16 20 3eqtr3d 
 |-  ( ( ph /\ A C_ B ) -> ( ( ( subringAlg ` R ) ` C ) |`s B ) = ( ( subringAlg ` R ) ` C ) )
22 1 oveq2i 
 |-  ( R |`s A ) = ( R |`s ( Base ` R ) )
23 5 elexd 
 |-  ( ph -> R e. _V )
24 eqid 
 |-  ( Base ` R ) = ( Base ` R )
25 24 ressid 
 |-  ( R e. _V -> ( R |`s ( Base ` R ) ) = R )
26 23 25 syl 
 |-  ( ph -> ( R |`s ( Base ` R ) ) = R )
27 22 26 eqtrid 
 |-  ( ph -> ( R |`s A ) = R )
28 27 adantr 
 |-  ( ( ph /\ A C_ B ) -> ( R |`s A ) = R )
29 15 oveq2d 
 |-  ( ( ph /\ A C_ B ) -> ( R |`s A ) = ( R |`s B ) )
30 29 2 eqtr4di 
 |-  ( ( ph /\ A C_ B ) -> ( R |`s A ) = S )
31 28 30 eqtr3d 
 |-  ( ( ph /\ A C_ B ) -> R = S )
32 31 fveq2d 
 |-  ( ( ph /\ A C_ B ) -> ( subringAlg ` R ) = ( subringAlg ` S ) )
33 32 fveq1d 
 |-  ( ( ph /\ A C_ B ) -> ( ( subringAlg ` R ) ` C ) = ( ( subringAlg ` S ) ` C ) )
34 21 33 eqtr2d 
 |-  ( ( ph /\ A C_ B ) -> ( ( subringAlg ` S ) ` C ) = ( ( ( subringAlg ` R ) ` C ) |`s B ) )
35 simpr 
 |-  ( ( ph /\ -. A C_ B ) -> -. A C_ B )
36 23 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> R e. _V )
37 1 fvexi 
 |-  A e. _V
38 37 a1i 
 |-  ( ph -> A e. _V )
39 38 3 ssexd 
 |-  ( ph -> B e. _V )
40 39 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> B e. _V )
41 2 1 ressval2 
 |-  ( ( -. A C_ B /\ R e. _V /\ B e. _V ) -> S = ( R sSet <. ( Base ` ndx ) , ( B i^i A ) >. ) )
42 35 36 40 41 syl3anc 
 |-  ( ( ph /\ -. A C_ B ) -> S = ( R sSet <. ( Base ` ndx ) , ( B i^i A ) >. ) )
43 dfss2 
 |-  ( B C_ A <-> ( B i^i A ) = B )
44 3 43 sylib 
 |-  ( ph -> ( B i^i A ) = B )
45 44 opeq2d 
 |-  ( ph -> <. ( Base ` ndx ) , ( B i^i A ) >. = <. ( Base ` ndx ) , B >. )
46 45 oveq2d 
 |-  ( ph -> ( R sSet <. ( Base ` ndx ) , ( B i^i A ) >. ) = ( R sSet <. ( Base ` ndx ) , B >. ) )
47 46 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> ( R sSet <. ( Base ` ndx ) , ( B i^i A ) >. ) = ( R sSet <. ( Base ` ndx ) , B >. ) )
48 42 47 eqtrd 
 |-  ( ( ph /\ -. A C_ B ) -> S = ( R sSet <. ( Base ` ndx ) , B >. ) )
49 2 oveq1i 
 |-  ( S |`s C ) = ( ( R |`s B ) |`s C )
50 ressabs 
 |-  ( ( B e. _V /\ C C_ B ) -> ( ( R |`s B ) |`s C ) = ( R |`s C ) )
51 39 4 50 syl2anc 
 |-  ( ph -> ( ( R |`s B ) |`s C ) = ( R |`s C ) )
52 49 51 eqtrid 
 |-  ( ph -> ( S |`s C ) = ( R |`s C ) )
53 52 opeq2d 
 |-  ( ph -> <. ( Scalar ` ndx ) , ( S |`s C ) >. = <. ( Scalar ` ndx ) , ( R |`s C ) >. )
54 53 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> <. ( Scalar ` ndx ) , ( S |`s C ) >. = <. ( Scalar ` ndx ) , ( R |`s C ) >. )
55 48 54 oveq12d 
 |-  ( ( ph /\ -. A C_ B ) -> ( S sSet <. ( Scalar ` ndx ) , ( S |`s C ) >. ) = ( ( R sSet <. ( Base ` ndx ) , B >. ) sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) )
56 scandxnbasendx 
 |-  ( Scalar ` ndx ) =/= ( Base ` ndx )
57 56 a1i 
 |-  ( ph -> ( Scalar ` ndx ) =/= ( Base ` ndx ) )
58 ovexd 
 |-  ( ph -> ( R |`s C ) e. _V )
59 fvex 
 |-  ( Scalar ` ndx ) e. _V
60 fvex 
 |-  ( Base ` ndx ) e. _V
61 59 60 setscom 
 |-  ( ( ( R e. _V /\ ( Scalar ` ndx ) =/= ( Base ` ndx ) ) /\ ( ( R |`s C ) e. _V /\ B e. _V ) ) -> ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( Base ` ndx ) , B >. ) = ( ( R sSet <. ( Base ` ndx ) , B >. ) sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) )
62 23 57 58 39 61 syl22anc 
 |-  ( ph -> ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( Base ` ndx ) , B >. ) = ( ( R sSet <. ( Base ` ndx ) , B >. ) sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) )
63 62 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( Base ` ndx ) , B >. ) = ( ( R sSet <. ( Base ` ndx ) , B >. ) sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) )
64 55 63 eqtr4d 
 |-  ( ( ph /\ -. A C_ B ) -> ( S sSet <. ( Scalar ` ndx ) , ( S |`s C ) >. ) = ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( Base ` ndx ) , B >. ) )
65 eqid 
 |-  ( .r ` R ) = ( .r ` R )
66 2 65 ressmulr 
 |-  ( B e. _V -> ( .r ` R ) = ( .r ` S ) )
67 39 66 syl 
 |-  ( ph -> ( .r ` R ) = ( .r ` S ) )
68 67 eqcomd 
 |-  ( ph -> ( .r ` S ) = ( .r ` R ) )
69 68 opeq2d 
 |-  ( ph -> <. ( .s ` ndx ) , ( .r ` S ) >. = <. ( .s ` ndx ) , ( .r ` R ) >. )
70 69 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> <. ( .s ` ndx ) , ( .r ` S ) >. = <. ( .s ` ndx ) , ( .r ` R ) >. )
71 64 70 oveq12d 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( S sSet <. ( Scalar ` ndx ) , ( S |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` S ) >. ) = ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( Base ` ndx ) , B >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) )
72 ovexd 
 |-  ( ph -> ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) e. _V )
73 vscandxnbasendx 
 |-  ( .s ` ndx ) =/= ( Base ` ndx )
74 73 a1i 
 |-  ( ph -> ( .s ` ndx ) =/= ( Base ` ndx ) )
75 fvexd 
 |-  ( ph -> ( .r ` R ) e. _V )
76 fvex 
 |-  ( .s ` ndx ) e. _V
77 76 60 setscom 
 |-  ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) e. _V /\ ( .s ` ndx ) =/= ( Base ` ndx ) ) /\ ( ( .r ` R ) e. _V /\ B e. _V ) ) -> ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) = ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( Base ` ndx ) , B >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) )
78 72 74 75 39 77 syl22anc 
 |-  ( ph -> ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) = ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( Base ` ndx ) , B >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) )
79 78 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) = ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( Base ` ndx ) , B >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) )
80 71 79 eqtr4d 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( S sSet <. ( Scalar ` ndx ) , ( S |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` S ) >. ) = ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) )
81 68 opeq2d 
 |-  ( ph -> <. ( .i ` ndx ) , ( .r ` S ) >. = <. ( .i ` ndx ) , ( .r ` R ) >. )
82 81 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> <. ( .i ` ndx ) , ( .r ` S ) >. = <. ( .i ` ndx ) , ( .r ` R ) >. )
83 80 82 oveq12d 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( ( S sSet <. ( Scalar ` ndx ) , ( S |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` S ) >. ) sSet <. ( .i ` ndx ) , ( .r ` S ) >. ) = ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) )
84 ovexd 
 |-  ( ph -> ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) e. _V )
85 ipndxnbasendx 
 |-  ( .i ` ndx ) =/= ( Base ` ndx )
86 85 a1i 
 |-  ( ph -> ( .i ` ndx ) =/= ( Base ` ndx ) )
87 fvex 
 |-  ( .i ` ndx ) e. _V
88 87 60 setscom 
 |-  ( ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) e. _V /\ ( .i ` ndx ) =/= ( Base ` ndx ) ) /\ ( ( .r ` R ) e. _V /\ B e. _V ) ) -> ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) = ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) )
89 84 86 75 39 88 syl22anc 
 |-  ( ph -> ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) = ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) )
90 89 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) = ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) )
91 83 90 eqtr4d 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( ( S sSet <. ( Scalar ` ndx ) , ( S |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` S ) >. ) sSet <. ( .i ` ndx ) , ( .r ` S ) >. ) = ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) )
92 2 ovexi 
 |-  S e. _V
93 2 1 ressbas2 
 |-  ( B C_ A -> B = ( Base ` S ) )
94 3 93 syl 
 |-  ( ph -> B = ( Base ` S ) )
95 4 94 sseqtrd 
 |-  ( ph -> C C_ ( Base ` S ) )
96 95 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> C C_ ( Base ` S ) )
97 sraval 
 |-  ( ( S e. _V /\ C C_ ( Base ` S ) ) -> ( ( subringAlg ` S ) ` C ) = ( ( ( S sSet <. ( Scalar ` ndx ) , ( S |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` S ) >. ) sSet <. ( .i ` ndx ) , ( .r ` S ) >. ) )
98 92 96 97 sylancr 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( subringAlg ` S ) ` C ) = ( ( ( S sSet <. ( Scalar ` ndx ) , ( S |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` S ) >. ) sSet <. ( .i ` ndx ) , ( .r ` S ) >. ) )
99 10 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> A = ( Base ` ( ( subringAlg ` R ) ` C ) ) )
100 99 sseq1d 
 |-  ( ( ph /\ -. A C_ B ) -> ( A C_ B <-> ( Base ` ( ( subringAlg ` R ) ` C ) ) C_ B ) )
101 35 100 mtbid 
 |-  ( ( ph /\ -. A C_ B ) -> -. ( Base ` ( ( subringAlg ` R ) ` C ) ) C_ B )
102 fvexd 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( subringAlg ` R ) ` C ) e. _V )
103 eqid 
 |-  ( ( ( subringAlg ` R ) ` C ) |`s B ) = ( ( ( subringAlg ` R ) ` C ) |`s B )
104 103 18 ressval2 
 |-  ( ( -. ( Base ` ( ( subringAlg ` R ) ` C ) ) C_ B /\ ( ( subringAlg ` R ) ` C ) e. _V /\ B e. _V ) -> ( ( ( subringAlg ` R ) ` C ) |`s B ) = ( ( ( subringAlg ` R ) ` C ) sSet <. ( Base ` ndx ) , ( B i^i ( Base ` ( ( subringAlg ` R ) ` C ) ) ) >. ) )
105 101 102 40 104 syl3anc 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( ( subringAlg ` R ) ` C ) |`s B ) = ( ( ( subringAlg ` R ) ` C ) sSet <. ( Base ` ndx ) , ( B i^i ( Base ` ( ( subringAlg ` R ) ` C ) ) ) >. ) )
106 10 ineq2d 
 |-  ( ph -> ( B i^i A ) = ( B i^i ( Base ` ( ( subringAlg ` R ) ` C ) ) ) )
107 106 44 eqtr3d 
 |-  ( ph -> ( B i^i ( Base ` ( ( subringAlg ` R ) ` C ) ) ) = B )
108 107 opeq2d 
 |-  ( ph -> <. ( Base ` ndx ) , ( B i^i ( Base ` ( ( subringAlg ` R ) ` C ) ) ) >. = <. ( Base ` ndx ) , B >. )
109 108 oveq2d 
 |-  ( ph -> ( ( ( subringAlg ` R ) ` C ) sSet <. ( Base ` ndx ) , ( B i^i ( Base ` ( ( subringAlg ` R ) ` C ) ) ) >. ) = ( ( ( subringAlg ` R ) ` C ) sSet <. ( Base ` ndx ) , B >. ) )
110 109 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( ( subringAlg ` R ) ` C ) sSet <. ( Base ` ndx ) , ( B i^i ( Base ` ( ( subringAlg ` R ) ` C ) ) ) >. ) = ( ( ( subringAlg ` R ) ` C ) sSet <. ( Base ` ndx ) , B >. ) )
111 sraval 
 |-  ( ( R e. V /\ C C_ ( Base ` R ) ) -> ( ( subringAlg ` R ) ` C ) = ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) )
112 5 8 111 syl2anc 
 |-  ( ph -> ( ( subringAlg ` R ) ` C ) = ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) )
113 112 oveq1d 
 |-  ( ph -> ( ( ( subringAlg ` R ) ` C ) sSet <. ( Base ` ndx ) , B >. ) = ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) )
114 113 adantr 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( ( subringAlg ` R ) ` C ) sSet <. ( Base ` ndx ) , B >. ) = ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) )
115 105 110 114 3eqtrd 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( ( subringAlg ` R ) ` C ) |`s B ) = ( ( ( ( R sSet <. ( Scalar ` ndx ) , ( R |`s C ) >. ) sSet <. ( .s ` ndx ) , ( .r ` R ) >. ) sSet <. ( .i ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , B >. ) )
116 91 98 115 3eqtr4d 
 |-  ( ( ph /\ -. A C_ B ) -> ( ( subringAlg ` S ) ` C ) = ( ( ( subringAlg ` R ) ` C ) |`s B ) )
117 34 116 pm2.61dan 
 |-  ( ph -> ( ( subringAlg ` S ) ` C ) = ( ( ( subringAlg ` R ) ` C ) |`s B ) )