Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rloccring Structured version   Visualization version   GIF version

Theorem rloccring 33256
Description: The ring localization 𝐿 of a commutative ring 𝑅 by a multiplicatively closed set 𝑆 is itself a commutative ring. (Contributed by Thierry Arnoux, 4-May-2025.)
Hypotheses
Ref Expression
rlocaddval.1 𝐵 = (Base‘𝑅)
rlocaddval.2 · = (.r𝑅)
rlocaddval.3 + = (+g𝑅)
rlocaddval.4 𝐿 = (𝑅 RLocal 𝑆)
rlocaddval.5 = (𝑅 ~RL 𝑆)
rlocaddval.r (𝜑𝑅 ∈ CRing)
rlocaddval.s (𝜑𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
Assertion
Ref Expression
rloccring (𝜑𝐿 ∈ CRing)

Proof of Theorem rloccring
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑥 𝑦 𝑧 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rlocaddval.1 . . 3 𝐵 = (Base‘𝑅)
2 eqid 2734 . . 3 (0g𝑅) = (0g𝑅)
3 rlocaddval.2 . . 3 · = (.r𝑅)
4 eqid 2734 . . 3 (-g𝑅) = (-g𝑅)
5 eqid 2734 . . 3 (𝐵 × 𝑆) = (𝐵 × 𝑆)
6 rlocaddval.4 . . 3 𝐿 = (𝑅 RLocal 𝑆)
7 rlocaddval.5 . . 3 = (𝑅 ~RL 𝑆)
8 rlocaddval.r . . 3 (𝜑𝑅 ∈ CRing)
9 rlocaddval.s . . . 4 (𝜑𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
10 eqid 2734 . . . . . 6 (mulGrp‘𝑅) = (mulGrp‘𝑅)
1110, 1mgpbas 20157 . . . . 5 𝐵 = (Base‘(mulGrp‘𝑅))
1211submss 18834 . . . 4 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → 𝑆𝐵)
139, 12syl 17 . . 3 (𝜑𝑆𝐵)
141, 2, 3, 4, 5, 6, 7, 8, 13rlocbas 33253 . 2 (𝜑 → ((𝐵 × 𝑆) / ) = (Base‘𝐿))
15 eqidd 2735 . 2 (𝜑 → (+g𝐿) = (+g𝐿))
16 eqidd 2735 . 2 (𝜑 → (.r𝐿) = (.r𝐿))
17 eqid 2734 . . . 4 (Base‘𝐿) = (Base‘𝐿)
18 eqid 2734 . . . 4 (0g𝐿) = (0g𝐿)
19 eqid 2734 . . . 4 (+g𝐿) = (+g𝐿)
208crngringd 20263 . . . . . . . 8 (𝜑𝑅 ∈ Ring)
211, 2ring0cl 20280 . . . . . . . 8 (𝑅 ∈ Ring → (0g𝑅) ∈ 𝐵)
2220, 21syl 17 . . . . . . 7 (𝜑 → (0g𝑅) ∈ 𝐵)
23 eqid 2734 . . . . . . . . . 10 (1r𝑅) = (1r𝑅)
2410, 23ringidval 20200 . . . . . . . . 9 (1r𝑅) = (0g‘(mulGrp‘𝑅))
2524subm0cl 18836 . . . . . . . 8 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → (1r𝑅) ∈ 𝑆)
269, 25syl 17 . . . . . . 7 (𝜑 → (1r𝑅) ∈ 𝑆)
2722, 26opelxpd 5727 . . . . . 6 (𝜑 → ⟨(0g𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆))
287ovexi 7464 . . . . . . 7 ∈ V
2928ecelqsi 8811 . . . . . 6 (⟨(0g𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆) → [⟨(0g𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
3027, 29syl 17 . . . . 5 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
3130, 14eleqtrd 2840 . . . 4 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] ∈ (Base‘𝐿))
3214eleq2d 2824 . . . . . 6 (𝜑 → (𝑥 ∈ ((𝐵 × 𝑆) / ) ↔ 𝑥 ∈ (Base‘𝐿)))
3332biimpar 477 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐿)) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
34 simpr 484 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
3534oveq2d 7446 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ))
3620ad4antr 732 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ Ring)
379ad4antr 732 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
3837, 12syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑆𝐵)
39 simplr 769 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏𝑆)
4038, 39sseldd 3995 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏𝐵)
411, 3, 2, 36, 40ringlzd 20308 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · 𝑏) = (0g𝑅))
42 simpllr 776 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎𝐵)
431, 3, 23, 36, 42ringridmd 20286 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑎 · (1r𝑅)) = 𝑎)
4441, 43oveq12d 7448 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))) = ((0g𝑅)(+g𝑅)𝑎))
45 eqid 2734 . . . . . . . . . . . 12 (+g𝑅) = (+g𝑅)
4636ringgrpd 20259 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ Grp)
471, 45, 2, 46, 42grplidd 18999 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅)(+g𝑅)𝑎) = 𝑎)
4844, 47eqtrd 2774 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))) = 𝑎)
491, 3, 23, 36, 40ringlidmd 20285 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((1r𝑅) · 𝑏) = 𝑏)
5048, 49opeq12d 4885 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩ = ⟨𝑎, 𝑏⟩)
5150eceq1d 8783 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩] = [⟨𝑎, 𝑏⟩] )
528ad4antr 732 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ CRing)
5322ad4antr 732 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (0g𝑅) ∈ 𝐵)
5437, 25syl 17 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (1r𝑅) ∈ 𝑆)
551, 3, 45, 6, 7, 52, 37, 53, 42, 54, 39, 19rlocaddval 33254 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩] )
5651, 55, 343eqtr4d 2784 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = 𝑥)
5735, 56eqtrd 2774 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
58 simpr 484 . . . . . . 7 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
5958elrlocbasi 33252 . . . . . 6 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
6057, 59r19.29vva 3213 . . . . 5 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
6133, 60syldan 591 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐿)) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
62 rlocaddval.3 . . . . . . . 8 + = (+g𝑅)
631, 3, 62, 6, 7, 52, 37, 42, 53, 39, 54, 19rlocaddval 33254 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
6434oveq1d 7445 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ))
6543, 41oveq12d 7448 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)) = (𝑎 + (0g𝑅)))
661, 62, 2, 46, 42grpridd 19000 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑎 + (0g𝑅)) = 𝑎)
6765, 66eqtr2d 2775 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎 = ((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)))
681, 3, 23, 36, 40ringridmd 20286 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · (1r𝑅)) = 𝑏)
6968eqcomd 2740 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏 = (𝑏 · (1r𝑅)))
7067, 69opeq12d 4885 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨𝑎, 𝑏⟩ = ⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩)
7170eceq1d 8783 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨𝑎, 𝑏⟩] = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
7234, 71eqtrd 2774 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑥 = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
7363, 64, 723eqtr4d 2784 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7473, 59r19.29vva 3213 . . . . 5 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7533, 74syldan 591 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐿)) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7617, 18, 19, 31, 61, 75ismgmid2 18693 . . 3 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] = (0g𝐿))
77 simp-4r 784 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
78 simpr 484 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑦 = [⟨𝑐, 𝑑⟩] )
7977, 78oveq12d 7448 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(+g𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ))
808ad8antr 740 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ CRing)
819ad8antr 740 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
82 simp-6r 788 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑎𝐵)
83 simpllr 776 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑐𝐵)
84 simp-5r 786 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑏𝑆)
85 simplr 769 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑑𝑆)
861, 3, 62, 6, 7, 80, 81, 82, 83, 84, 85, 19rlocaddval 33254 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] )
8780crnggrpd 20264 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ Grp)
8820ad8antr 740 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ Ring)
8981, 12syl 17 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑆𝐵)
9089, 85sseldd 3995 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑑𝐵)
911, 3, 88, 82, 90ringcld 20276 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑑) ∈ 𝐵)
9289, 84sseldd 3995 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑏𝐵)
931, 3, 88, 83, 92ringcld 20276 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑐 · 𝑏) ∈ 𝐵)
941, 62, 87, 91, 93grpcld 18977 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ 𝐵)
9510, 3mgpplusg 20155 . . . . . . . . . . . 12 · = (+g‘(mulGrp‘𝑅))
9695, 81, 84, 85submcld 33022 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑏 · 𝑑) ∈ 𝑆)
9794, 96opelxpd 5727 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆))
9828ecelqsi 8811 . . . . . . . . . 10 (⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆) → [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
9997, 98syl 17 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
10086, 99eqeltrd 2838 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) ∈ ((𝐵 × 𝑆) / ))
10179, 100eqeltrd 2838 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
102 simp-4r 784 . . . . . . . 8 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
103102elrlocbasi 33252 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑐𝐵𝑑𝑆 𝑦 = [⟨𝑐, 𝑑⟩] )
104101, 103r19.29vva 3213 . . . . . 6 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
105 simplr 769 . . . . . . 7 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
106105elrlocbasi 33252 . . . . . 6 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
107104, 106r19.29vva 3213 . . . . 5 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
1081073impa 1109 . . . 4 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
1098ad10antr 744 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ CRing)
110109crnggrpd 20264 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ Grp)
11120ad10antr 744 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ Ring)
112 simp-9r 794 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑎𝐵)
1139ad10antr 744 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
114113, 12syl 17 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑆𝐵)
115 simp-5r 786 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑑𝑆)
116114, 115sseldd 3995 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑑𝐵)
1171, 3, 111, 112, 116ringcld 20276 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑑) ∈ 𝐵)
118 simplr 769 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑓𝑆)
119114, 118sseldd 3995 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑓𝐵)
1201, 3, 111, 117, 119ringcld 20276 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑓) ∈ 𝐵)
121 simp-6r 788 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑐𝐵)
122 simp-8r 792 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑏𝑆)
123114, 122sseldd 3995 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑏𝐵)
1241, 3, 111, 121, 123ringcld 20276 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑏) ∈ 𝐵)
1251, 3, 111, 124, 119ringcld 20276 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑓) ∈ 𝐵)
126 simpllr 776 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑒𝐵)
1271, 3, 111, 123, 116ringcld 20276 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) ∈ 𝐵)
1281, 3, 111, 126, 127ringcld 20276 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) ∈ 𝐵)
1291, 62, 110, 120, 125, 128grpassd 18975 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))) = (((𝑎 · 𝑑) · 𝑓) + (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑)))))
1301, 3, 111, 112, 116, 119ringassd 20274 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑓) = (𝑎 · (𝑑 · 𝑓)))
1311, 3, 109, 121, 123, 119cringmul32d 33217 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑓) = ((𝑐 · 𝑓) · 𝑏))
1321, 3, 109, 126, 123, 116crng12d 20275 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) = (𝑏 · (𝑒 · 𝑑)))
1331, 3, 111, 126, 116ringcld 20276 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · 𝑑) ∈ 𝐵)
1341, 3, 109, 123, 133crngcomd 20272 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑒 · 𝑑)) = ((𝑒 · 𝑑) · 𝑏))
135132, 134eqtrd 2774 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) = ((𝑒 · 𝑑) · 𝑏))
136131, 135oveq12d 7448 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏)))
137130, 136oveq12d 7448 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑓) + (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑)))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
138129, 137eqtrd 2774 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
1391, 62, 3, 111, 117, 124, 119ringdird 33219 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) = (((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)))
140139oveq1d 7445 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))))
1411, 3, 111, 121, 119ringcld 20276 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑓) ∈ 𝐵)
1421, 62, 3, 111, 141, 133, 123ringdird 33219 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏) = (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏)))
143142oveq2d 7446 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
144138, 140, 1433eqtr4d 2784 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)))
1451, 3, 111, 123, 116, 119ringassd 20274 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = (𝑏 · (𝑑 · 𝑓)))
146144, 145opeq12d 4885 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩)
147146eceq1d 8783 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩] )
1481, 62, 110, 117, 124grpcld 18977 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ 𝐵)
14995, 113, 122, 115submcld 33022 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) ∈ 𝑆)
1501, 3, 62, 6, 7, 109, 113, 148, 126, 149, 118, 19rlocaddval 33254 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩] )
1511, 62, 110, 141, 133grpcld 18977 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑓) + (𝑒 · 𝑑)) ∈ 𝐵)
15295, 113, 115, 118submcld 33022 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑑 · 𝑓) ∈ 𝑆)
1531, 3, 62, 6, 7, 109, 113, 112, 151, 122, 152, 19rlocaddval 33254 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = [⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩] )
154147, 150, 1533eqtr4d 2784 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
1551, 3, 62, 6, 7, 109, 113, 112, 121, 122, 115, 19rlocaddval 33254 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] )
156155oveq1d 7445 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ))
1571, 3, 62, 6, 7, 109, 113, 121, 126, 115, 118, 19rlocaddval 33254 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] )
158157oveq2d 7446 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
159154, 156, 1583eqtr4d 2784 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
160 simp-7r 790 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
161 simp-4r 784 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑦 = [⟨𝑐, 𝑑⟩] )
162160, 161oveq12d 7448 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(+g𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ))
163 simpr 484 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑧 = [⟨𝑒, 𝑓⟩] )
164162, 163oveq12d 7448 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ))
165161, 163oveq12d 7448 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑦(+g𝐿)𝑧) = ([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ))
166160, 165oveq12d 7448 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
167159, 164, 1663eqtr4d 2784 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
168 simpr3 1195 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑧 ∈ ((𝐵 × 𝑆) / ))
169168ad6antr 736 . . . . . . . 8 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑧 ∈ ((𝐵 × 𝑆) / ))
170169elrlocbasi 33252 . . . . . . 7 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ∃𝑒𝐵𝑓𝑆 𝑧 = [⟨𝑒, 𝑓⟩] )
171167, 170r19.29vva 3213 . . . . . 6 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
172 simpr2 1194 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
173172ad5ant12 756 . . . . . . 7 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
174173elrlocbasi 33252 . . . . . 6 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑐𝐵𝑑𝑆 𝑦 = [⟨𝑐, 𝑑⟩] )
175171, 174r19.29vva 3213 . . . . 5 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
176 simpr1 1193 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
177176elrlocbasi 33252 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
178175, 177r19.29vva 3213 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
17914, 15, 108, 178, 30, 60, 74ismndd 18781 . . 3 (𝜑𝐿 ∈ Mnd)
180 eqid 2734 . . . . . . . 8 (invg𝑅) = (invg𝑅)
1811, 180, 46, 42grpinvcld 19018 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((invg𝑅)‘𝑎) ∈ 𝐵)
182181, 39opelxpd 5727 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((invg𝑅)‘𝑎), 𝑏⟩ ∈ (𝐵 × 𝑆))
18328ecelqsi 8811 . . . . . 6 (⟨((invg𝑅)‘𝑎), 𝑏⟩ ∈ (𝐵 × 𝑆) → [⟨((invg𝑅)‘𝑎), 𝑏⟩] ∈ ((𝐵 × 𝑆) / ))
184182, 183syl 17 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((invg𝑅)‘𝑎), 𝑏⟩] ∈ ((𝐵 × 𝑆) / ))
185 simpr 484 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] )
186 simplr 769 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
187185, 186oveq12d 7448 . . . . . 6 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → (𝑢(+g𝐿)𝑥) = ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ))
188187eqeq1d 2736 . . . . 5 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → ((𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] ↔ ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(0g𝑅), (1r𝑅)⟩] ))
1891, 3, 62, 6, 7, 52, 37, 181, 42, 39, 39, 19rlocaddval 33254 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩] )
1901, 62, 2, 180, 46, 42grplinvd 19024 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((invg𝑅)‘𝑎) + 𝑎) = (0g𝑅))
191190oveq1d 7445 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) + 𝑎) · 𝑏) = ((0g𝑅) · 𝑏))
1921, 62, 3, 36, 181, 42, 40ringdird 33219 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) + 𝑎) · 𝑏) = ((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)))
193191, 192, 413eqtr3d 2782 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)) = (0g𝑅))
194193opeq1d 4883 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩ = ⟨(0g𝑅), (𝑏 · 𝑏)⟩)
195194eceq1d 8783 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩] = [⟨(0g𝑅), (𝑏 · 𝑏)⟩] )
1961, 2, 23, 3, 4, 5, 7, 8, 9erler 33251 . . . . . . . 8 (𝜑 Er (𝐵 × 𝑆))
197196ad4antr 732 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → Er (𝐵 × 𝑆))
198 eqidd 2735 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (𝑏 · 𝑏)⟩ = ⟨(0g𝑅), (𝑏 · 𝑏)⟩)
199 eqidd 2735 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (1r𝑅)⟩ = ⟨(0g𝑅), (1r𝑅)⟩)
20095, 37, 39, 39submcld 33022 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · 𝑏) ∈ 𝑆)
2011, 3, 23, 36, 53ringridmd 20286 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · (1r𝑅)) = (0g𝑅))
20238, 200sseldd 3995 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · 𝑏) ∈ 𝐵)
2031, 3, 2, 36, 202ringlzd 20308 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · (𝑏 · 𝑏)) = (0g𝑅))
204201, 203oveq12d 7448 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏))) = ((0g𝑅)(-g𝑅)(0g𝑅)))
2051, 2, 4grpsubid 19054 . . . . . . . . . . . 12 ((𝑅 ∈ Grp ∧ (0g𝑅) ∈ 𝐵) → ((0g𝑅)(-g𝑅)(0g𝑅)) = (0g𝑅))
20646, 53, 205syl2anc 584 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅)(-g𝑅)(0g𝑅)) = (0g𝑅))
207204, 206eqtrd 2774 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏))) = (0g𝑅))
208207oveq2d 7446 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏)))) = ((𝑏 · 𝑏) · (0g𝑅)))
2091, 3, 2, 36, 202ringrzd 20309 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (0g𝑅)) = (0g𝑅))
210208, 209eqtrd 2774 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏)))) = (0g𝑅))
2111, 7, 38, 2, 3, 4, 198, 199, 53, 53, 200, 54, 200, 210erlbrd 33249 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (𝑏 · 𝑏)⟩ ⟨(0g𝑅), (1r𝑅)⟩)
212197, 211erthi 8796 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨(0g𝑅), (𝑏 · 𝑏)⟩] = [⟨(0g𝑅), (1r𝑅)⟩] )
213189, 195, 2123eqtrd 2778 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(0g𝑅), (1r𝑅)⟩] )
214184, 188, 213rspcedvd 3623 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑢 ∈ ((𝐵 × 𝑆) / )(𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] )
215214, 59r19.29vva 3213 . . 3 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ∃𝑢 ∈ ((𝐵 × 𝑆) / )(𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] )
21614, 15, 76, 179, 215isgrpd2e 18985 . 2 (𝜑𝐿 ∈ Grp)
21777, 78oveq12d 7448 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ))
218 eqid 2734 . . . . . . . 8 (.r𝐿) = (.r𝐿)
2191, 3, 62, 6, 7, 80, 81, 82, 83, 84, 85, 218rlocmulval 33255 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] )
2201, 3, 88, 82, 83ringcld 20276 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑐) ∈ 𝐵)
221220, 96opelxpd 5727 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆))
22228ecelqsi 8811 . . . . . . . 8 (⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
223221, 222syl 17 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
224219, 223eqeltrd 2838 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) ∈ ((𝐵 × 𝑆) / ))
225217, 224eqeltrd 2838 . . . . 5 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
226225, 103r19.29vva 3213 . . . 4 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
227226, 106r19.29vva 3213 . . 3 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
2282273impa 1109 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
2291, 3, 111, 112, 121, 126ringassd 20274 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑐) · 𝑒) = (𝑎 · (𝑐 · 𝑒)))
230229, 145opeq12d 4885 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩)
231230eceq1d 8783 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩] )
2321, 3, 111, 112, 121ringcld 20276 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑐) ∈ 𝐵)
2331, 3, 62, 6, 7, 109, 113, 232, 126, 149, 118, 218rlocmulval 33255 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] )
2341, 3, 111, 121, 126ringcld 20276 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑒) ∈ 𝐵)
2351, 3, 62, 6, 7, 109, 113, 112, 234, 122, 152, 218rlocmulval 33255 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ) = [⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩] )
236231, 233, 2353eqtr4d 2784 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
2371, 3, 62, 6, 7, 109, 113, 112, 121, 122, 115, 218rlocmulval 33255 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] )
238237oveq1d 7445 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
2391, 3, 62, 6, 7, 109, 113, 121, 126, 115, 118, 218rlocmulval 33255 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] )
240239oveq2d 7446 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
241236, 238, 2403eqtr4d 2784 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
242160, 161oveq12d 7448 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ))
243242, 163oveq12d 7448 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ))
244161, 163oveq12d 7448 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑦(.r𝐿)𝑧) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
245160, 244oveq12d 7448 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
246241, 243, 2453eqtr4d 2784 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
247246, 170r19.29vva 3213 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
248247, 174r19.29vva 3213 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
249248, 177r19.29vva 3213 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
250196ad10antr 744 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → Er (𝐵 × 𝑆))
251 eqidd 2735 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩ = ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩)
2521, 3, 111, 112, 123ringcld 20276 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑏) ∈ 𝐵)
2531, 62, 3, 111, 252, 141, 133ringdid 33218 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑏) · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) = (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))))
2541, 3, 111, 112, 123, 151ringassd 20274 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑏) · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
255253, 254eqtr3d 2776 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
25610crngmgp 20258 . . . . . . . . . . . . . . . 16 (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
2578, 256syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
258257ad10antr 744 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (mulGrp‘𝑅) ∈ CMnd)
25911, 95, 258, 112, 121, 123, 119cmn4d 33019 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑐) · (𝑏 · 𝑓)) = ((𝑎 · 𝑏) · (𝑐 · 𝑓)))
26011, 95, 258, 112, 126, 123, 116cmn4d 33019 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑏 · 𝑑)) = ((𝑎 · 𝑏) · (𝑒 · 𝑑)))
261259, 260oveq12d 7448 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))) = (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))))
2621, 3, 109, 123, 112, 151crng12d 20275 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
263255, 261, 2623eqtr4d 2784 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))) = (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
2641, 3, 109, 127, 123, 119crng12d 20275 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · (𝑏 · 𝑓)) = (𝑏 · ((𝑏 · 𝑑) · 𝑓)))
265145oveq2d 7446 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · ((𝑏 · 𝑑) · 𝑓)) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
266264, 265eqtrd 2774 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · (𝑏 · 𝑓)) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
267263, 266opeq12d 4885 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩ = ⟨(𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))), (𝑏 · (𝑏 · (𝑑 · 𝑓)))⟩)
2681, 3, 111, 112, 151ringcld 20276 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) ∈ 𝐵)
2691, 3, 111, 123, 268ringcld 20276 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) ∈ 𝐵)
27095, 113, 122, 152submcld 33022 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑑 · 𝑓)) ∈ 𝑆)
27195, 113, 122, 270submcld 33022 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑏 · (𝑑 · 𝑓))) ∈ 𝑆)
272 eqidd 2735 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) = (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
273 eqidd 2735 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑏 · (𝑑 · 𝑓))) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
2741, 7, 109, 113, 3, 251, 267, 268, 269, 270, 271, 122, 272, 273erlbr2d 33250 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩ ⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩)
275250, 274erthi 8796 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩] = [⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩] )
2761, 3, 62, 6, 7, 109, 113, 112, 151, 122, 152, 218rlocmulval 33255 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = [⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩] )
2771, 3, 111, 112, 126ringcld 20276 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑒) ∈ 𝐵)
27895, 113, 122, 118submcld 33022 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑓) ∈ 𝑆)
2791, 3, 62, 6, 7, 109, 113, 232, 277, 149, 278, 19rlocaddval 33254 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ) = [⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩] )
280275, 276, 2793eqtr4d 2784 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ))
281157oveq2d 7446 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
2821, 3, 62, 6, 7, 109, 113, 112, 126, 122, 118, 218rlocmulval 33255 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] )
283237, 282oveq12d 7448 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ))
284280, 281, 2833eqtr4d 2784 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
285160, 165oveq12d 7448 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
286160, 163oveq12d 7448 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)𝑧) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
287242, 286oveq12d 7448 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
288284, 285, 2873eqtr4d 2784 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
289288, 170r19.29vva 3213 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
290289, 174r19.29vva 3213 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
291290, 177r19.29vva 3213 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
2921, 62, 3, 111, 117, 124, 126ringdird 33219 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒) = (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)))
293292opeq1d 4883 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨(((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)), ((𝑏 · 𝑑) · 𝑓)⟩)
2941, 3, 111, 117, 126, 119ringassd 20274 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑒) · 𝑓) = ((𝑎 · 𝑑) · (𝑒 · 𝑓)))
2951, 3, 111, 117, 126ringcld 20276 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑒) ∈ 𝐵)
2961, 3, 109, 119, 295crngcomd 20272 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · ((𝑎 · 𝑑) · 𝑒)) = (((𝑎 · 𝑑) · 𝑒) · 𝑓))
29711, 95, 258, 112, 126, 116, 119cmn4d 33019 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑑 · 𝑓)) = ((𝑎 · 𝑑) · (𝑒 · 𝑓)))
298294, 296, 2973eqtr4rd 2785 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑑 · 𝑓)) = (𝑓 · ((𝑎 · 𝑑) · 𝑒)))
2991, 3, 111, 124, 126, 119ringassd 20274 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑏) · 𝑒) · 𝑓) = ((𝑐 · 𝑏) · (𝑒 · 𝑓)))
3001, 3, 111, 124, 126ringcld 20276 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑒) ∈ 𝐵)
3011, 3, 109, 119, 300crngcomd 20272 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · ((𝑐 · 𝑏) · 𝑒)) = (((𝑐 · 𝑏) · 𝑒) · 𝑓))
30211, 95, 258, 121, 126, 123, 119cmn4d 33019 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑒) · (𝑏 · 𝑓)) = ((𝑐 · 𝑏) · (𝑒 · 𝑓)))
303299, 301, 3023eqtr4rd 2785 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑒) · (𝑏 · 𝑓)) = (𝑓 · ((𝑐 · 𝑏) · 𝑒)))
304298, 303oveq12d 7448 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))) = ((𝑓 · ((𝑎 · 𝑑) · 𝑒)) + (𝑓 · ((𝑐 · 𝑏) · 𝑒))))
3051, 62, 3, 111, 119, 295, 300ringdid 33218 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) = ((𝑓 · ((𝑎 · 𝑑) · 𝑒)) + (𝑓 · ((𝑐 · 𝑏) · 𝑒))))
306304, 305eqtr4d 2777 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))) = (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))))
307114, 278sseldd 3995 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑓) ∈ 𝐵)
3081, 3, 111, 116, 307, 119ringassd 20274 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑑 · (𝑏 · 𝑓)) · 𝑓) = (𝑑 · ((𝑏 · 𝑓) · 𝑓)))
3091, 3, 109, 123, 116crngcomd 20272 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) = (𝑑 · 𝑏))
310309oveq1d 7445 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = ((𝑑 · 𝑏) · 𝑓))
3111, 3, 111, 116, 123, 119ringassd 20274 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑑 · 𝑏) · 𝑓) = (𝑑 · (𝑏 · 𝑓)))
312310, 311eqtrd 2774 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = (𝑑 · (𝑏 · 𝑓)))
313312oveq1d 7445 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) = ((𝑑 · (𝑏 · 𝑓)) · 𝑓))
3141, 3, 109, 307, 116, 119crng12d 20275 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑓) · (𝑑 · 𝑓)) = (𝑑 · ((𝑏 · 𝑓) · 𝑓)))
315308, 313, 3143eqtr4rd 2785 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑓) · (𝑑 · 𝑓)) = (((𝑏 · 𝑑) · 𝑓) · 𝑓))
316306, 315opeq12d 4885 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩ = ⟨(𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))), (((𝑏 · 𝑑) · 𝑓) · 𝑓)⟩)
3171, 62, 110, 295, 300grpcld 18977 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)) ∈ 𝐵)
3181, 3, 111, 119, 317ringcld 20276 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) ∈ 𝐵)
319145, 270eqeltrd 2838 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) ∈ 𝑆)
32095, 113, 319, 118submcld 33022 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) ∈ 𝑆)
321 eqidd 2735 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) = (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))))
322114, 319sseldd 3995 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) ∈ 𝐵)
3231, 3, 109, 322, 119crngcomd 20272 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) = (𝑓 · ((𝑏 · 𝑑) · 𝑓)))
3241, 7, 109, 113, 3, 293, 316, 317, 318, 319, 320, 118, 321, 323erlbr2d 33250 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ ⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩)
325250, 324erthi 8796 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩] )
3261, 3, 62, 6, 7, 109, 113, 148, 126, 149, 118, 218rlocmulval 33255 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] )
3271, 3, 62, 6, 7, 109, 113, 277, 234, 278, 152, 19rlocaddval 33254 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ) = [⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩] )
328325, 326, 3273eqtr4d 2784 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
329155oveq1d 7445 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
330282, 239oveq12d 7448 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
331328, 329, 3303eqtr4d 2784 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
332162, 163oveq12d 7448 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ))
333286, 244oveq12d 7448 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
334331, 332, 3333eqtr4d 2784 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
335334, 170r19.29vva 3213 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
336335, 174r19.29vva 3213 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
337336, 177r19.29vva 3213 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
33813, 26sseldd 3995 . . . 4 (𝜑 → (1r𝑅) ∈ 𝐵)
339338, 26opelxpd 5727 . . 3 (𝜑 → ⟨(1r𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆))
34028ecelqsi 8811 . . 3 (⟨(1r𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆) → [⟨(1r𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
341339, 340syl 17 . 2 (𝜑 → [⟨(1r𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
34234oveq2d 7446 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
3431, 3, 23, 36, 42ringlidmd 20285 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((1r𝑅) · 𝑎) = 𝑎)
344343, 49opeq12d 4885 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩ = ⟨𝑎, 𝑏⟩)
345344eceq1d 8783 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩] = [⟨𝑎, 𝑏⟩] )
34638, 54sseldd 3995 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (1r𝑅) ∈ 𝐵)
3471, 3, 62, 6, 7, 52, 37, 346, 42, 54, 39, 218rlocmulval 33255 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩] )
348345, 347, 343eqtr4d 2784 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = 𝑥)
349342, 348eqtrd 2774 . . 3 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = 𝑥)
350349, 59r19.29vva 3213 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = 𝑥)
3511, 3, 62, 6, 7, 52, 37, 42, 346, 39, 54, 218rlocmulval 33255 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = [⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩] )
35234oveq1d 7445 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ))
35343eqcomd 2740 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎 = (𝑎 · (1r𝑅)))
354353, 69opeq12d 4885 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨𝑎, 𝑏⟩ = ⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩)
355354eceq1d 8783 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨𝑎, 𝑏⟩] = [⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩] )
356351, 352, 3553eqtr4d 2784 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = [⟨𝑎, 𝑏⟩] )
357356, 34eqtr4d 2777 . . 3 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = 𝑥)
358357, 59r19.29vva 3213 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = 𝑥)
3591, 3, 80, 82, 83crngcomd 20272 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑐) = (𝑐 · 𝑎))
3601, 3, 80, 92, 90crngcomd 20272 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑏 · 𝑑) = (𝑑 · 𝑏))
361359, 360opeq12d 4885 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ = ⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩)
362361eceq1d 8783 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] = [⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩] )
3631, 3, 62, 6, 7, 80, 81, 83, 82, 85, 84, 218rlocmulval 33255 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩] )
364362, 219, 3633eqtr4d 2784 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
36578, 77oveq12d 7448 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑦(.r𝐿)𝑥) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
366364, 217, 3653eqtr4d 2784 . . . . 5 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
367366, 103r19.29vva 3213 . . . 4 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
368367, 106r19.29vva 3213 . . 3 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
3693683impa 1109 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
37014, 15, 16, 216, 228, 249, 291, 337, 341, 350, 358, 369iscrngd 20305 1 (𝜑𝐿 ∈ CRing)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086   = wceq 1536  wcel 2105  wrex 3067  wss 3962  cop 4636   × cxp 5686  cfv 6562  (class class class)co 7430   Er wer 8740  [cec 8741   / cqs 8742  Basecbs 17244  +gcplusg 17297  .rcmulr 17298  0gc0g 17485  SubMndcsubmnd 18807  Grpcgrp 18963  invgcminusg 18964  -gcsg 18965  CMndccmn 19812  mulGrpcmgp 20151  1rcur 20198  Ringcrg 20250  CRingccrg 20251   ~RL cerl 33239   RLocal crloc 33240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-ec 8745  df-qs 8749  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-fz 13544  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-0g 17487  df-imas 17554  df-qus 17555  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-grp 18966  df-minusg 18967  df-sbg 18968  df-cmn 19814  df-abl 19815  df-mgp 20152  df-rng 20170  df-ur 20199  df-ring 20252  df-cring 20253  df-erl 33241  df-rloc 33242
This theorem is referenced by:  rloc0g  33257  rloc1r  33258  rlocf1  33259  fracfld  33289
  Copyright terms: Public domain W3C validator