Metamath Proof Explorer

Theorem 0mplrim

Description: Build a ring isomorphism between multivariate polynomials with no variables and the underlying ring. (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Hypotheses 0mplric.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
0mplric.p ⊢ 𝑃 = ( ∅ mPoly 𝑅 )
0mplric.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
0mplrim.f ⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑝 ‘ ∅ ) )
Assertion 0mplrim ( 𝜑 → 𝐹 ∈ ( 𝑃 RingIso 𝑅 ) )

Proof

Step Hyp Ref Expression
1 0mplric.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
2 0mplric.p ⊢ 𝑃 = ( ∅ mPoly 𝑅 )
3 0mplric.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 0mplrim.f ⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑝 ‘ ∅ ) )
5 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
6 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
7 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
8 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9 0ex ⊢ ∅ ∈ V
10 9 a1i ⊢ ( 𝜑 → ∅ ∈ V )
11 2 10 3 mplringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
12 fveq1 ⊢ ( 𝑝 = ( 1r ‘ 𝑃 ) → ( 𝑝 ‘ ∅ ) = ( ( 1r ‘ 𝑃 ) ‘ ∅ ) )
13 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
14 2 13 6 5 10 3 mplascl1 ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
15 14 fveq1d ⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ‘ ∅ ) = ( ( 1r ‘ 𝑃 ) ‘ ∅ ) )
16 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 }
17 16 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
18 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
19 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
20 19 6 3 ringidcld ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
21 2 17 18 19 13 10 3 20 mplascl ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } ↦ if ( 𝑝 = ( ∅ × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑝 = ∅ ) → 𝑝 = ∅ )
23 0xp ⊢ ( ∅ × { 0 } ) = ∅
24 22 23 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑝 = ∅ ) → 𝑝 = ( ∅ × { 0 } ) )
25 24 iftrued ⊢ ( ( 𝜑 ∧ 𝑝 = ∅ ) → if ( 𝑝 = ( ∅ × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
26 breq1 ⊢ ( ℎ = ∅ → ( ℎ finSupp 0 ↔ ∅ finSupp 0 ) )
27 nn0ex ⊢ ℕ0 ∈ V
28 27 a1i ⊢ ( ⊤ → ℕ0 ∈ V )
29 9 a1i ⊢ ( ⊤ → ∅ ∈ V )
30 f0 ⊢ ∅ : ∅ ⟶ ℕ0
31 30 a1i ⊢ ( ⊤ → ∅ : ∅ ⟶ ℕ0 )
32 28 29 31 elmapdd ⊢ ( ⊤ → ∅ ∈ ( ℕ0 ↑m ∅ ) )
33 0fi ⊢ ∅ ∈ Fin
34 33 a1i ⊢ ( ⊤ → ∅ ∈ Fin )
35 c0ex ⊢ 0 ∈ V
36 35 a1i ⊢ ( ⊤ → 0 ∈ V )
37 31 34 36 fidmfisupp ⊢ ( ⊤ → ∅ finSupp 0 )
38 26 32 37 elrabd ⊢ ( ⊤ → ∅ ∈ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } )
39 38 mptru ⊢ ∅ ∈ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 }
40 39 a1i ⊢ ( 𝜑 → ∅ ∈ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } )
41 21 25 40 20 fvmptd ⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ‘ ∅ ) = ( 1r ‘ 𝑅 ) )
42 15 41 eqtr3d ⊢ ( 𝜑 → ( ( 1r ‘ 𝑃 ) ‘ ∅ ) = ( 1r ‘ 𝑅 ) )
43 12 42 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑝 = ( 1r ‘ 𝑃 ) ) → ( 𝑝 ‘ ∅ ) = ( 1r ‘ 𝑅 ) )
44 1 5 11 ringidcld ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) ∈ 𝐵 )
45 4 43 44 20 fvmptd2 ⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑃 ) ) = ( 1r ‘ 𝑅 ) )
46 fveq1 ⊢ ( 𝑝 = ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) → ( 𝑝 ‘ ∅ ) = ( ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ‘ ∅ ) )
47 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑃 ∈ Ring )
48 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
49 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
50 1 7 47 48 49 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 )
51 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ‘ ∅ ) ∈ V )
52 4 46 50 51 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ‘ ∅ ) )
53 elsni ⊢ ( 𝑝 ∈ { ∅ } → 𝑝 = ∅ )
54 39 a1i ⊢ ( 𝑝 ∈ { ∅ } → ∅ ∈ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } )
55 53 54 eqeltrd ⊢ ( 𝑝 ∈ { ∅ } → 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } )
56 ssrab2 ⊢ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m ∅ )
57 mapdm0 ⊢ ( ℕ0 ∈ V → ( ℕ0 ↑m ∅ ) = { ∅ } )
58 27 57 ax-mp ⊢ ( ℕ0 ↑m ∅ ) = { ∅ }
59 56 58 sseqtri ⊢ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } ⊆ { ∅ }
60 59 sseli ⊢ ( 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } → 𝑝 ∈ { ∅ } )
61 55 60 impbii ⊢ ( 𝑝 ∈ { ∅ } ↔ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 } )
62 61 eqriv ⊢ { ∅ } = { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ℎ finSupp 0 }
63 62 psrbasfsupp ⊢ { ∅ } = { ℎ ∈ ( ℕ0 ↑m ∅ ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
64 2 1 8 7 63 48 49 mplmul ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) = ( 𝑝 ∈ { ∅ } ↦ ( 𝑅 Σg ( 𝑞 ∈ { 𝑟 ∈ { ∅ } ∣ 𝑟 ∘r ≤ 𝑝 } ↦ ( ( 𝑥 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ ( 𝑝 ∘f − 𝑞 ) ) ) ) ) ) )
65 3 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
66 65 grpmndd ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
67 66 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → 𝑅 ∈ Mnd )
68 9 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → ∅ ∈ V )
69 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → 𝑅 ∈ Ring )
70 2 19 1 63 48 mplelf ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 : { ∅ } ⟶ ( Base ‘ 𝑅 ) )
71 70 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → 𝑥 : { ∅ } ⟶ ( Base ‘ 𝑅 ) )
72 9 snid ⊢ ∅ ∈ { ∅ }
73 72 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → ∅ ∈ { ∅ } )
74 71 73 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → ( 𝑥 ‘ ∅ ) ∈ ( Base ‘ 𝑅 ) )
75 2 19 1 63 49 mplelf ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 : { ∅ } ⟶ ( Base ‘ 𝑅 ) )
76 75 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → 𝑦 : { ∅ } ⟶ ( Base ‘ 𝑅 ) )
77 76 73 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → ( 𝑦 ‘ ∅ ) ∈ ( Base ‘ 𝑅 ) )
78 19 8 69 74 77 ringcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → ( ( 𝑥 ‘ ∅ ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ ∅ ) ) ∈ ( Base ‘ 𝑅 ) )
79 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → 𝑞 = ∅ )
80 79 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → ( 𝑥 ‘ 𝑞 ) = ( 𝑥 ‘ ∅ ) )
81 9 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → ∅ ∈ V )
82 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → 𝑝 = ∅ )
83 82 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → ∅ = 𝑝 )
84 30 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → ∅ : ∅ ⟶ ℕ0 )
85 83 84 feq1dd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → 𝑝 : ∅ ⟶ ℕ0 )
86 85 ffnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → 𝑝 Fn ∅ )
87 79 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → ∅ = 𝑞 )
88 87 84 feq1dd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → 𝑞 : ∅ ⟶ ℕ0 )
89 88 ffnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → 𝑞 Fn ∅ )
90 81 86 89 offvalfv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → ( 𝑝 ∘f − 𝑞 ) = ( 𝑎 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑎 ) − ( 𝑞 ‘ 𝑎 ) ) ) )
91 mpt0 ⊢ ( 𝑎 ∈ ∅ ↦ ( ( 𝑝 ‘ 𝑎 ) − ( 𝑞 ‘ 𝑎 ) ) ) = ∅
92 90 91 eqtrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → ( 𝑝 ∘f − 𝑞 ) = ∅ )
93 92 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → ( 𝑦 ‘ ( 𝑝 ∘f − 𝑞 ) ) = ( 𝑦 ‘ ∅ ) )
94 80 93 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑞 = ∅ ) → ( ( 𝑥 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ ( 𝑝 ∘f − 𝑞 ) ) ) = ( ( 𝑥 ‘ ∅ ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ ∅ ) ) )
95 19 67 68 78 94 gsumsnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → ( 𝑅 Σg ( 𝑞 ∈ { ∅ } ↦ ( ( 𝑥 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ ( 𝑝 ∘f − 𝑞 ) ) ) ) ) = ( ( 𝑥 ‘ ∅ ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ ∅ ) ) )
96 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) ∧ 𝑎 ∈ ∅ ) → 𝑎 ∈ ∅ )
97 noel ⊢ ¬ 𝑎 ∈ ∅
98 97 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) ∧ 𝑎 ∈ ∅ ) → ¬ 𝑎 ∈ ∅ )
99 96 98 pm2.21dd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) ∧ 𝑎 ∈ ∅ ) → ( 𝑟 ‘ 𝑎 ) ≤ ( 𝑝 ‘ 𝑎 ) )
100 99 ralrimiva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → ∀ 𝑎 ∈ ∅ ( 𝑟 ‘ 𝑎 ) ≤ ( 𝑝 ‘ 𝑎 ) )
101 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → 𝑟 ∈ { ∅ } )
102 101 elsnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → 𝑟 = ∅ )
103 102 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → ∅ = 𝑟 )
104 30 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → ∅ : ∅ ⟶ ℕ0 )
105 103 104 feq1dd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → 𝑟 : ∅ ⟶ ℕ0 )
106 105 ffnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → 𝑟 Fn ∅ )
107 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → 𝑝 = ∅ )
108 107 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → ∅ = 𝑝 )
109 108 104 feq1dd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → 𝑝 : ∅ ⟶ ℕ0 )
110 109 ffnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → 𝑝 Fn ∅ )
111 vex ⊢ 𝑝 ∈ V
112 111 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → 𝑝 ∈ V )
113 inidm ⊢ ( ∅ ∩ ∅ ) = ∅
114 eqidd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) ∧ 𝑎 ∈ ∅ ) → ( 𝑟 ‘ 𝑎 ) = ( 𝑟 ‘ 𝑎 ) )
115 eqidd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) ∧ 𝑎 ∈ ∅ ) → ( 𝑝 ‘ 𝑎 ) = ( 𝑝 ‘ 𝑎 ) )
116 106 110 101 112 113 114 115 ofrfvalg ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → ( 𝑟 ∘r ≤ 𝑝 ↔ ∀ 𝑎 ∈ ∅ ( 𝑟 ‘ 𝑎 ) ≤ ( 𝑝 ‘ 𝑎 ) ) )
117 100 116 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) ∧ 𝑟 ∈ { ∅ } ) → 𝑟 ∘r ≤ 𝑝 )
118 117 rabeqcda ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → { 𝑟 ∈ { ∅ } ∣ 𝑟 ∘r ≤ 𝑝 } = { ∅ } )
119 118 mpteq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → ( 𝑞 ∈ { 𝑟 ∈ { ∅ } ∣ 𝑟 ∘r ≤ 𝑝 } ↦ ( ( 𝑥 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ ( 𝑝 ∘f − 𝑞 ) ) ) ) = ( 𝑞 ∈ { ∅ } ↦ ( ( 𝑥 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ ( 𝑝 ∘f − 𝑞 ) ) ) ) )
120 119 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → ( 𝑅 Σg ( 𝑞 ∈ { 𝑟 ∈ { ∅ } ∣ 𝑟 ∘r ≤ 𝑝 } ↦ ( ( 𝑥 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ ( 𝑝 ∘f − 𝑞 ) ) ) ) ) = ( 𝑅 Σg ( 𝑞 ∈ { ∅ } ↦ ( ( 𝑥 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ ( 𝑝 ∘f − 𝑞 ) ) ) ) ) )
121 fveq1 ⊢ ( 𝑝 = 𝑥 → ( 𝑝 ‘ ∅ ) = ( 𝑥 ‘ ∅ ) )
122 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ‘ ∅ ) ∈ V )
123 4 121 48 122 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝑥 ‘ ∅ ) )
124 123 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝑥 ‘ ∅ ) )
125 fveq1 ⊢ ( 𝑝 = 𝑦 → ( 𝑝 ‘ ∅ ) = ( 𝑦 ‘ ∅ ) )
126 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ‘ ∅ ) ∈ V )
127 4 125 49 126 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 ‘ ∅ ) )
128 127 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 ‘ ∅ ) )
129 124 128 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝑥 ‘ ∅ ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ ∅ ) ) )
130 95 120 129 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ∅ ) → ( 𝑅 Σg ( 𝑞 ∈ { 𝑟 ∈ { ∅ } ∣ 𝑟 ∘r ≤ 𝑝 } ↦ ( ( 𝑥 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ ( 𝑝 ∘f − 𝑞 ) ) ) ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) )
131 72 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ∅ ∈ { ∅ } )
132 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) ∈ V )
133 64 130 131 132 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ‘ ∅ ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) )
134 52 133 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) )
135 134 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) )
136 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
137 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
138 fvexd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 ‘ ∅ ) ∈ V )
139 snex ⊢ { ⟨ ∅ , 𝑎 ⟩ } ∈ V
140 139 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → { ⟨ ∅ , 𝑎 ⟩ } ∈ V )
141 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → 𝑎 = ( 𝑝 ‘ ∅ ) )
142 simplr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → 𝑝 ∈ 𝐵 )
143 2 19 1 63 142 mplelf ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → 𝑝 : { ∅ } ⟶ ( Base ‘ 𝑅 ) )
144 72 a1i ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → ∅ ∈ { ∅ } )
145 143 144 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → ( 𝑝 ‘ ∅ ) ∈ ( Base ‘ 𝑅 ) )
146 141 145 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
147 146 elexd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → 𝑎 ∈ V )
148 fvsng ⊢ ( ( ∅ ∈ V ∧ 𝑎 ∈ V ) → ( { ⟨ ∅ , 𝑎 ⟩ } ‘ ∅ ) = 𝑎 )
149 9 147 148 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → ( { ⟨ ∅ , 𝑎 ⟩ } ‘ ∅ ) = 𝑎 )
150 149 141 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → ( 𝑝 ‘ ∅ ) = ( { ⟨ ∅ , 𝑎 ⟩ } ‘ ∅ ) )
151 9 a1i ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → ∅ ∈ V )
152 eqid ⊢ { ∅ } = { ∅ }
153 143 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → 𝑝 Fn { ∅ } )
154 151 147 fsnd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → { ⟨ ∅ , 𝑎 ⟩ } : { ∅ } ⟶ V )
155 154 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → { ⟨ ∅ , 𝑎 ⟩ } Fn { ∅ } )
156 151 152 153 155 fsneq ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → ( 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } ↔ ( 𝑝 ‘ ∅ ) = ( { ⟨ ∅ , 𝑎 ⟩ } ‘ ∅ ) ) )
157 150 156 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } )
158 146 157 jca ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } ) )
159 158 anasss ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } ) )
160 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } ) → 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } )
161 fvexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( Base ‘ 𝑅 ) ∈ V )
162 snex ⊢ { ∅ } ∈ V
163 162 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → { ∅ } ∈ V )
164 9 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ∅ ∈ V )
165 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
166 164 165 fsnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → { ⟨ ∅ , 𝑎 ⟩ } : { ∅ } ⟶ ( Base ‘ 𝑅 ) )
167 161 163 166 elmapdd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → { ⟨ ∅ , 𝑎 ⟩ } ∈ ( ( Base ‘ 𝑅 ) ↑m { ∅ } ) )
168 eqid ⊢ ( ∅ mPwSer 𝑅 ) = ( ∅ mPwSer 𝑅 )
169 eqid ⊢ ( Base ‘ ( ∅ mPwSer 𝑅 ) ) = ( Base ‘ ( ∅ mPwSer 𝑅 ) )
170 168 19 63 169 164 psrbas ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( Base ‘ ( ∅ mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑m { ∅ } ) )
171 167 170 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → { ⟨ ∅ , 𝑎 ⟩ } ∈ ( Base ‘ ( ∅ mPwSer 𝑅 ) ) )
172 fvexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
173 snopfsupp ⊢ ( ( ∅ ∈ V ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ ( 0g ‘ 𝑅 ) ∈ V ) → { ⟨ ∅ , 𝑎 ⟩ } finSupp ( 0g ‘ 𝑅 ) )
174 9 165 172 173 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → { ⟨ ∅ , 𝑎 ⟩ } finSupp ( 0g ‘ 𝑅 ) )
175 2 168 169 18 1 mplelbas ⊢ ( { ⟨ ∅ , 𝑎 ⟩ } ∈ 𝐵 ↔ ( { ⟨ ∅ , 𝑎 ⟩ } ∈ ( Base ‘ ( ∅ mPwSer 𝑅 ) ) ∧ { ⟨ ∅ , 𝑎 ⟩ } finSupp ( 0g ‘ 𝑅 ) ) )
176 171 174 175 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → { ⟨ ∅ , 𝑎 ⟩ } ∈ 𝐵 )
177 176 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } ) → { ⟨ ∅ , 𝑎 ⟩ } ∈ 𝐵 )
178 160 177 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } ) → 𝑝 ∈ 𝐵 )
179 160 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } ) → ( 𝑝 ‘ ∅ ) = ( { ⟨ ∅ , 𝑎 ⟩ } ‘ ∅ ) )
180 fvsng ⊢ ( ( ∅ ∈ V ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( { ⟨ ∅ , 𝑎 ⟩ } ‘ ∅ ) = 𝑎 )
181 9 165 180 sylancr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( { ⟨ ∅ , 𝑎 ⟩ } ‘ ∅ ) = 𝑎 )
182 181 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } ) → ( { ⟨ ∅ , 𝑎 ⟩ } ‘ ∅ ) = 𝑎 )
183 179 182 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } ) → 𝑎 = ( 𝑝 ‘ ∅ ) )
184 178 183 jca ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } ) → ( 𝑝 ∈ 𝐵 ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) )
185 184 anasss ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } ) ) → ( 𝑝 ∈ 𝐵 ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) )
186 159 185 impbida ⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝐵 ∧ 𝑎 = ( 𝑝 ‘ ∅ ) ) ↔ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑝 = { ⟨ ∅ , 𝑎 ⟩ } ) ) )
187 4 138 140 186 f1od ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ ( Base ‘ 𝑅 ) )
188 f1of ⊢ ( 𝐹 : 𝐵 –1-1-onto→ ( Base ‘ 𝑅 ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
189 187 188 syl ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
190 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) → 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) )
191 190 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) → ( 𝑝 ‘ ∅ ) = ( ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ‘ ∅ ) )
192 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) → 𝑥 ∈ 𝐵 )
193 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) → 𝑦 ∈ 𝐵 )
194 2 1 137 136 192 193 mpladd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) )
195 194 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) → ( ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ‘ ∅ ) = ( ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) ‘ ∅ ) )
196 70 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 Fn { ∅ } )
197 75 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 Fn { ∅ } )
198 162 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → { ∅ } ∈ V )
199 inidm ⊢ ( { ∅ } ∩ { ∅ } ) = { ∅ }
200 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ∅ ∈ { ∅ } ) → ( 𝑥 ‘ ∅ ) = ( 𝑥 ‘ ∅ ) )
201 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ∅ ∈ { ∅ } ) → ( 𝑦 ‘ ∅ ) = ( 𝑦 ‘ ∅ ) )
202 196 197 198 198 199 200 201 ofval ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ∅ ∈ { ∅ } ) → ( ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) ‘ ∅ ) = ( ( 𝑥 ‘ ∅ ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ ∅ ) ) )
203 72 202 mpan2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) ‘ ∅ ) = ( ( 𝑥 ‘ ∅ ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ ∅ ) ) )
204 203 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) → ( ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) ‘ ∅ ) = ( ( 𝑥 ‘ ∅ ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ ∅ ) ) )
205 191 195 204 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) → ( 𝑝 ‘ ∅ ) = ( ( 𝑥 ‘ ∅ ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ ∅ ) ) )
206 11 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
207 206 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑃 ∈ Grp )
208 1 136 207 48 49 grpcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 )
209 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ‘ ∅ ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ ∅ ) ) ∈ V )
210 4 205 208 209 fvmptd2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝑥 ‘ ∅ ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ ∅ ) ) )
211 123 127 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝑥 ‘ ∅ ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ ∅ ) ) )
212 210 211 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) )
213 212 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) )
214 1 5 6 7 8 11 3 45 135 19 136 137 189 213 isrhmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑅 ) )
215 1 19 isrim ⊢ ( 𝐹 ∈ ( 𝑃 RingIso 𝑅 ) ↔ ( 𝐹 ∈ ( 𝑃 RingHom 𝑅 ) ∧ 𝐹 : 𝐵 –1-1-onto→ ( Base ‘ 𝑅 ) ) )
216 214 187 215 sylanbrc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingIso 𝑅 ) )