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

Metamath Proof Explorer

Theorem evlseu

Description: For a given interpretation of the variables G and of the scalars F , this extends to a homomorphic interpretation of the polynomial ring in exactly one way. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses evlseu.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
evlseu.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
evlseu.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
evlseu.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
evlseu.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
evlseu.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evlseu.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlseu.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
evlseu.g ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
Assertion evlseu ( 𝜑 → ∃! 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) )

Proof

Step Hyp Ref Expression
1 evlseu.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 evlseu.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 evlseu.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
4 evlseu.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
5 evlseu.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6 evlseu.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
7 evlseu.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
8 evlseu.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
9 evlseu.g ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
10 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
11 eqid ⊢ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } = { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin }
12 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
13 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑆 ) ) = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
14 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
15 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) )
16 1 10 2 11 12 13 14 4 15 5 6 7 8 9 3 evlslem1 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∈ ( 𝑃 RingHom 𝑆 ) ∧ ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∘ 𝐴 ) = 𝐹 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∘ 𝑉 ) = 𝐺 ) )
17 coeq1 ⊢ ( 𝑚 = ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) → ( 𝑚 ∘ 𝐴 ) = ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∘ 𝐴 ) )
18 17 eqeq1d ⊢ ( 𝑚 = ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) → ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ↔ ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∘ 𝐴 ) = 𝐹 ) )
19 coeq1 ⊢ ( 𝑚 = ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) → ( 𝑚 ∘ 𝑉 ) = ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∘ 𝑉 ) )
20 19 eqeq1d ⊢ ( 𝑚 = ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) → ( ( 𝑚 ∘ 𝑉 ) = 𝐺 ↔ ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∘ 𝑉 ) = 𝐺 ) )
21 18 20 anbi12d ⊢ ( 𝑚 = ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) → ( ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) ↔ ( ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∘ 𝐴 ) = 𝐹 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∘ 𝑉 ) = 𝐺 ) ) )
22 21 rspcev ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∈ ( 𝑃 RingHom 𝑆 ) ∧ ( ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∘ 𝐴 ) = 𝐹 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∘ 𝑉 ) = 𝐺 ) ) → ∃ 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) )
23 22 3impb ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∈ ( 𝑃 RingHom 𝑆 ) ∧ ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∘ 𝐴 ) = 𝐹 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↦ ( 𝑆 Σg ( 𝑦 ∈ { 𝑧 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑧 “ ℕ ) ∈ Fin } ↦ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑦 ) ) ( .r ‘ 𝑆 ) ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑦 ∘f ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝐺 ) ) ) ) ) ) ∘ 𝑉 ) = 𝐺 ) → ∃ 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) )
24 16 23 syl ⊢ ( 𝜑 → ∃ 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) )
25 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
26 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
27 6 26 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
28 1 10 25 3 5 27 mplasclf ⊢ ( 𝜑 → 𝐴 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) )
29 28 ffund ⊢ ( 𝜑 → Fun 𝐴 )
30 funcoeqres ⊢ ( ( Fun 𝐴 ∧ ( 𝑚 ∘ 𝐴 ) = 𝐹 ) → ( 𝑚 ↾ ran 𝐴 ) = ( 𝐹 ∘ ◡ 𝐴 ) )
31 29 30 sylan ⊢ ( ( 𝜑 ∧ ( 𝑚 ∘ 𝐴 ) = 𝐹 ) → ( 𝑚 ↾ ran 𝐴 ) = ( 𝐹 ∘ ◡ 𝐴 ) )
32 1 4 10 5 27 mvrf2 ⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ ( Base ‘ 𝑃 ) )
33 32 ffund ⊢ ( 𝜑 → Fun 𝑉 )
34 funcoeqres ⊢ ( ( Fun 𝑉 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) → ( 𝑚 ↾ ran 𝑉 ) = ( 𝐺 ∘ ◡ 𝑉 ) )
35 33 34 sylan ⊢ ( ( 𝜑 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) → ( 𝑚 ↾ ran 𝑉 ) = ( 𝐺 ∘ ◡ 𝑉 ) )
36 31 35 anim12dan ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) ) → ( ( 𝑚 ↾ ran 𝐴 ) = ( 𝐹 ∘ ◡ 𝐴 ) ∧ ( 𝑚 ↾ ran 𝑉 ) = ( 𝐺 ∘ ◡ 𝑉 ) ) )
37 36 ex ⊢ ( 𝜑 → ( ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) → ( ( 𝑚 ↾ ran 𝐴 ) = ( 𝐹 ∘ ◡ 𝐴 ) ∧ ( 𝑚 ↾ ran 𝑉 ) = ( 𝐺 ∘ ◡ 𝑉 ) ) ) )
38 resundi ⊢ ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝑚 ↾ ran 𝐴 ) ∪ ( 𝑚 ↾ ran 𝑉 ) )
39 uneq12 ⊢ ( ( ( 𝑚 ↾ ran 𝐴 ) = ( 𝐹 ∘ ◡ 𝐴 ) ∧ ( 𝑚 ↾ ran 𝑉 ) = ( 𝐺 ∘ ◡ 𝑉 ) ) → ( ( 𝑚 ↾ ran 𝐴 ) ∪ ( 𝑚 ↾ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) )
40 38 39 eqtrid ⊢ ( ( ( 𝑚 ↾ ran 𝐴 ) = ( 𝐹 ∘ ◡ 𝐴 ) ∧ ( 𝑚 ↾ ran 𝑉 ) = ( 𝐺 ∘ ◡ 𝑉 ) ) → ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) )
41 37 40 syl6 ⊢ ( 𝜑 → ( ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) → ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ) )
42 41 ralrimivw ⊢ ( 𝜑 → ∀ 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) → ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ) )
43 eqtr3 ⊢ ( ( ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ∧ ( 𝑛 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ) → ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( 𝑛 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) )
44 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
45 44 5 6 psrassa ⊢ ( 𝜑 → ( 𝐼 mPwSer 𝑅 ) ∈ AssAlg )
46 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
47 44 4 46 5 27 mvrf ⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
48 47 frnd ⊢ ( 𝜑 → ran 𝑉 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
49 eqid ⊢ ( AlgSpan ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( AlgSpan ‘ ( 𝐼 mPwSer 𝑅 ) )
50 eqid ⊢ ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) )
51 eqid ⊢ ( mrCls ‘ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ) = ( mrCls ‘ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
52 49 50 51 46 aspval2 ⊢ ( ( ( 𝐼 mPwSer 𝑅 ) ∈ AssAlg ∧ ran 𝑉 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( ( AlgSpan ‘ ( 𝐼 mPwSer 𝑅 ) ) ‘ ran 𝑉 ) = ( ( mrCls ‘ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ‘ ( ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) ∪ ran 𝑉 ) ) )
53 45 48 52 syl2anc ⊢ ( 𝜑 → ( ( AlgSpan ‘ ( 𝐼 mPwSer 𝑅 ) ) ‘ ran 𝑉 ) = ( ( mrCls ‘ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ‘ ( ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) ∪ ran 𝑉 ) ) )
54 1 44 4 49 5 6 mplbas2 ⊢ ( 𝜑 → ( ( AlgSpan ‘ ( 𝐼 mPwSer 𝑅 ) ) ‘ ran 𝑉 ) = ( Base ‘ 𝑃 ) )
55 44 1 10 5 27 mplsubrg ⊢ ( 𝜑 → ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
56 1 44 10 mplval2 ⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑃 ) )
57 56 subsubrg2 ⊢ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) → ( SubRing ‘ 𝑃 ) = ( ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∩ 𝒫 ( Base ‘ 𝑃 ) ) )
58 55 57 syl ⊢ ( 𝜑 → ( SubRing ‘ 𝑃 ) = ( ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∩ 𝒫 ( Base ‘ 𝑃 ) ) )
59 58 fveq2d ⊢ ( 𝜑 → ( mrCls ‘ ( SubRing ‘ 𝑃 ) ) = ( mrCls ‘ ( ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∩ 𝒫 ( Base ‘ 𝑃 ) ) ) )
60 50 56 ressascl ⊢ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) → ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( algSc ‘ 𝑃 ) )
61 55 60 syl ⊢ ( 𝜑 → ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( algSc ‘ 𝑃 ) )
62 3 61 eqtr4id ⊢ ( 𝜑 → 𝐴 = ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) )
63 62 rneqd ⊢ ( 𝜑 → ran 𝐴 = ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) )
64 63 uneq1d ⊢ ( 𝜑 → ( ran 𝐴 ∪ ran 𝑉 ) = ( ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) ∪ ran 𝑉 ) )
65 59 64 fveq12d ⊢ ( 𝜑 → ( ( mrCls ‘ ( SubRing ‘ 𝑃 ) ) ‘ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( mrCls ‘ ( ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∩ 𝒫 ( Base ‘ 𝑃 ) ) ) ‘ ( ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) ∪ ran 𝑉 ) ) )
66 assaring ⊢ ( ( 𝐼 mPwSer 𝑅 ) ∈ AssAlg → ( 𝐼 mPwSer 𝑅 ) ∈ Ring )
67 46 subrgmre ⊢ ( ( 𝐼 mPwSer 𝑅 ) ∈ Ring → ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∈ ( Moore ‘ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) )
68 45 66 67 3syl ⊢ ( 𝜑 → ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∈ ( Moore ‘ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) )
69 28 frnd ⊢ ( 𝜑 → ran 𝐴 ⊆ ( Base ‘ 𝑃 ) )
70 63 69 eqsstrrd ⊢ ( 𝜑 → ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) ⊆ ( Base ‘ 𝑃 ) )
71 32 frnd ⊢ ( 𝜑 → ran 𝑉 ⊆ ( Base ‘ 𝑃 ) )
72 70 71 unssd ⊢ ( 𝜑 → ( ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) ∪ ran 𝑉 ) ⊆ ( Base ‘ 𝑃 ) )
73 eqid ⊢ ( mrCls ‘ ( ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∩ 𝒫 ( Base ‘ 𝑃 ) ) ) = ( mrCls ‘ ( ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∩ 𝒫 ( Base ‘ 𝑃 ) ) )
74 51 73 submrc ⊢ ( ( ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∈ ( Moore ‘ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) ∪ ran 𝑉 ) ⊆ ( Base ‘ 𝑃 ) ) → ( ( mrCls ‘ ( ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∩ 𝒫 ( Base ‘ 𝑃 ) ) ) ‘ ( ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) ∪ ran 𝑉 ) ) = ( ( mrCls ‘ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ‘ ( ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) ∪ ran 𝑉 ) ) )
75 68 55 72 74 syl3anc ⊢ ( 𝜑 → ( ( mrCls ‘ ( ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∩ 𝒫 ( Base ‘ 𝑃 ) ) ) ‘ ( ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) ∪ ran 𝑉 ) ) = ( ( mrCls ‘ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ‘ ( ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) ∪ ran 𝑉 ) ) )
76 65 75 eqtr2d ⊢ ( 𝜑 → ( ( mrCls ‘ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ‘ ( ran ( algSc ‘ ( 𝐼 mPwSer 𝑅 ) ) ∪ ran 𝑉 ) ) = ( ( mrCls ‘ ( SubRing ‘ 𝑃 ) ) ‘ ( ran 𝐴 ∪ ran 𝑉 ) ) )
77 53 54 76 3eqtr3d ⊢ ( 𝜑 → ( Base ‘ 𝑃 ) = ( ( mrCls ‘ ( SubRing ‘ 𝑃 ) ) ‘ ( ran 𝐴 ∪ ran 𝑉 ) ) )
78 77 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) ∧ ( ran 𝐴 ∪ ran 𝑉 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) ) → ( Base ‘ 𝑃 ) = ( ( mrCls ‘ ( SubRing ‘ 𝑃 ) ) ‘ ( ran 𝐴 ∪ ran 𝑉 ) ) )
79 1 5 27 mplringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
80 10 subrgmre ⊢ ( 𝑃 ∈ Ring → ( SubRing ‘ 𝑃 ) ∈ ( Moore ‘ ( Base ‘ 𝑃 ) ) )
81 79 80 syl ⊢ ( 𝜑 → ( SubRing ‘ 𝑃 ) ∈ ( Moore ‘ ( Base ‘ 𝑃 ) ) )
82 81 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) ∧ ( ran 𝐴 ∪ ran 𝑉 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) ) → ( SubRing ‘ 𝑃 ) ∈ ( Moore ‘ ( Base ‘ 𝑃 ) ) )
83 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) ∧ ( ran 𝐴 ∪ ran 𝑉 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) ) → ( ran 𝐴 ∪ ran 𝑉 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) )
84 rhmeql ⊢ ( ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) → dom ( 𝑚 ∩ 𝑛 ) ∈ ( SubRing ‘ 𝑃 ) )
85 84 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) ∧ ( ran 𝐴 ∪ ran 𝑉 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) ) → dom ( 𝑚 ∩ 𝑛 ) ∈ ( SubRing ‘ 𝑃 ) )
86 eqid ⊢ ( mrCls ‘ ( SubRing ‘ 𝑃 ) ) = ( mrCls ‘ ( SubRing ‘ 𝑃 ) )
87 86 mrcsscl ⊢ ( ( ( SubRing ‘ 𝑃 ) ∈ ( Moore ‘ ( Base ‘ 𝑃 ) ) ∧ ( ran 𝐴 ∪ ran 𝑉 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) ∧ dom ( 𝑚 ∩ 𝑛 ) ∈ ( SubRing ‘ 𝑃 ) ) → ( ( mrCls ‘ ( SubRing ‘ 𝑃 ) ) ‘ ( ran 𝐴 ∪ ran 𝑉 ) ) ⊆ dom ( 𝑚 ∩ 𝑛 ) )
88 82 83 85 87 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) ∧ ( ran 𝐴 ∪ ran 𝑉 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) ) → ( ( mrCls ‘ ( SubRing ‘ 𝑃 ) ) ‘ ( ran 𝐴 ∪ ran 𝑉 ) ) ⊆ dom ( 𝑚 ∩ 𝑛 ) )
89 78 88 eqsstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) ∧ ( ran 𝐴 ∪ ran 𝑉 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) ) → ( Base ‘ 𝑃 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) )
90 89 ex ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) → ( ( ran 𝐴 ∪ ran 𝑉 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) → ( Base ‘ 𝑃 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) ) )
91 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) → 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) )
92 10 2 rhmf ⊢ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) → 𝑚 : ( Base ‘ 𝑃 ) ⟶ 𝐶 )
93 ffn ⊢ ( 𝑚 : ( Base ‘ 𝑃 ) ⟶ 𝐶 → 𝑚 Fn ( Base ‘ 𝑃 ) )
94 91 92 93 3syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) → 𝑚 Fn ( Base ‘ 𝑃 ) )
95 simprr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) → 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) )
96 10 2 rhmf ⊢ ( 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) → 𝑛 : ( Base ‘ 𝑃 ) ⟶ 𝐶 )
97 ffn ⊢ ( 𝑛 : ( Base ‘ 𝑃 ) ⟶ 𝐶 → 𝑛 Fn ( Base ‘ 𝑃 ) )
98 95 96 97 3syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) → 𝑛 Fn ( Base ‘ 𝑃 ) )
99 69 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) → ran 𝐴 ⊆ ( Base ‘ 𝑃 ) )
100 71 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) → ran 𝑉 ⊆ ( Base ‘ 𝑃 ) )
101 99 100 unssd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) → ( ran 𝐴 ∪ ran 𝑉 ) ⊆ ( Base ‘ 𝑃 ) )
102 fnreseql ⊢ ( ( 𝑚 Fn ( Base ‘ 𝑃 ) ∧ 𝑛 Fn ( Base ‘ 𝑃 ) ∧ ( ran 𝐴 ∪ ran 𝑉 ) ⊆ ( Base ‘ 𝑃 ) ) → ( ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( 𝑛 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) ↔ ( ran 𝐴 ∪ ran 𝑉 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) ) )
103 94 98 101 102 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) → ( ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( 𝑛 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) ↔ ( ran 𝐴 ∪ ran 𝑉 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) ) )
104 fneqeql2 ⊢ ( ( 𝑚 Fn ( Base ‘ 𝑃 ) ∧ 𝑛 Fn ( Base ‘ 𝑃 ) ) → ( 𝑚 = 𝑛 ↔ ( Base ‘ 𝑃 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) ) )
105 94 98 104 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) → ( 𝑚 = 𝑛 ↔ ( Base ‘ 𝑃 ) ⊆ dom ( 𝑚 ∩ 𝑛 ) ) )
106 90 103 105 3imtr4d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) → ( ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( 𝑛 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) → 𝑚 = 𝑛 ) )
107 43 106 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∧ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ) ) → ( ( ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ∧ ( 𝑛 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ) → 𝑚 = 𝑛 ) )
108 107 ralrimivva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∀ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ( ( ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ∧ ( 𝑛 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ) → 𝑚 = 𝑛 ) )
109 reseq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( 𝑛 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) )
110 109 eqeq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ↔ ( 𝑛 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ) )
111 110 rmo4 ⊢ ( ∃* 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ↔ ∀ 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ∀ 𝑛 ∈ ( 𝑃 RingHom 𝑆 ) ( ( ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ∧ ( 𝑛 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ) → 𝑚 = 𝑛 ) )
112 108 111 sylibr ⊢ ( 𝜑 → ∃* 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) )
113 rmoim ⊢ ( ∀ 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) → ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) ) → ( ∃* 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( 𝑚 ↾ ( ran 𝐴 ∪ ran 𝑉 ) ) = ( ( 𝐹 ∘ ◡ 𝐴 ) ∪ ( 𝐺 ∘ ◡ 𝑉 ) ) → ∃* 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) ) )
114 42 112 113 sylc ⊢ ( 𝜑 → ∃* 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) )
115 reu5 ⊢ ( ∃! 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) ↔ ( ∃ 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) ∧ ∃* 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) ) )
116 24 114 115 sylanbrc ⊢ ( 𝜑 → ∃! 𝑚 ∈ ( 𝑃 RingHom 𝑆 ) ( ( 𝑚 ∘ 𝐴 ) = 𝐹 ∧ ( 𝑚 ∘ 𝑉 ) = 𝐺 ) )