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 ⊢ 𝐴 = ( Base ‘ 𝑅 )
resssra.s ⊢ 𝑆 = ( 𝑅 ↾s 𝐵 )
resssra.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
resssra.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
resssra.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
Assertion resssra ( 𝜑 → ( ( subringAlg ‘ 𝑆 ) ‘ 𝐶 ) = ( ( ( subringAlg ‘ 𝑅 ) ‘ 𝐶 ) ↾s 𝐵 ) )

Proof

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