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 33242
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 2740 . . 3 (0g𝑅) = (0g𝑅)
3 rlocaddval.2 . . 3 · = (.r𝑅)
4 eqid 2740 . . 3 (-g𝑅) = (-g𝑅)
5 eqid 2740 . . 3 (𝐵 × 𝑆) = (𝐵 × 𝑆)
6 rlocaddval.4 . . 3 𝐿 = (𝑅 RLocal 𝑆)
7 rlocaddval.5 . . 3 = (𝑅 ~RL 𝑆)
8 rlocaddval.r . . 3 (𝜑𝑅 ∈ CRing)
9 rlocaddval.s . . . 4 (𝜑𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
10 eqid 2740 . . . . . 6 (mulGrp‘𝑅) = (mulGrp‘𝑅)
1110, 1mgpbas 20167 . . . . 5 𝐵 = (Base‘(mulGrp‘𝑅))
1211submss 18844 . . . 4 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → 𝑆𝐵)
139, 12syl 17 . . 3 (𝜑𝑆𝐵)
141, 2, 3, 4, 5, 6, 7, 8, 13rlocbas 33239 . 2 (𝜑 → ((𝐵 × 𝑆) / ) = (Base‘𝐿))
15 eqidd 2741 . 2 (𝜑 → (+g𝐿) = (+g𝐿))
16 eqidd 2741 . 2 (𝜑 → (.r𝐿) = (.r𝐿))
17 eqid 2740 . . . 4 (Base‘𝐿) = (Base‘𝐿)
18 eqid 2740 . . . 4 (0g𝐿) = (0g𝐿)
19 eqid 2740 . . . 4 (+g𝐿) = (+g𝐿)
208crngringd 20273 . . . . . . . 8 (𝜑𝑅 ∈ Ring)
211, 2ring0cl 20290 . . . . . . . 8 (𝑅 ∈ Ring → (0g𝑅) ∈ 𝐵)
2220, 21syl 17 . . . . . . 7 (𝜑 → (0g𝑅) ∈ 𝐵)
23 eqid 2740 . . . . . . . . . 10 (1r𝑅) = (1r𝑅)
2410, 23ringidval 20210 . . . . . . . . 9 (1r𝑅) = (0g‘(mulGrp‘𝑅))
2524subm0cl 18846 . . . . . . . 8 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → (1r𝑅) ∈ 𝑆)
269, 25syl 17 . . . . . . 7 (𝜑 → (1r𝑅) ∈ 𝑆)
2722, 26opelxpd 5739 . . . . . 6 (𝜑 → ⟨(0g𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆))
287ovexi 7482 . . . . . . 7 ∈ V
2928ecelqsi 8831 . . . . . 6 (⟨(0g𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆) → [⟨(0g𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
3027, 29syl 17 . . . . 5 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
3130, 14eleqtrd 2846 . . . 4 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] ∈ (Base‘𝐿))
3214eleq2d 2830 . . . . . 6 (𝜑 → (𝑥 ∈ ((𝐵 × 𝑆) / ) ↔ 𝑥 ∈ (Base‘𝐿)))
3332biimpar 477 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐿)) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
34 simpr 484 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
3534oveq2d 7464 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ))
3620ad4antr 731 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ Ring)
379ad4antr 731 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
3837, 12syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑆𝐵)
39 simplr 768 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏𝑆)
4038, 39sseldd 4009 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏𝐵)
411, 3, 2, 36, 40ringlzd 20318 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · 𝑏) = (0g𝑅))
42 simpllr 775 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎𝐵)
431, 3, 23, 36, 42ringridmd 20296 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑎 · (1r𝑅)) = 𝑎)
4441, 43oveq12d 7466 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))) = ((0g𝑅)(+g𝑅)𝑎))
45 eqid 2740 . . . . . . . . . . . 12 (+g𝑅) = (+g𝑅)
4636ringgrpd 20269 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ Grp)
471, 45, 2, 46, 42grplidd 19009 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅)(+g𝑅)𝑎) = 𝑎)
4844, 47eqtrd 2780 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))) = 𝑎)
491, 3, 23, 36, 40ringlidmd 20295 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((1r𝑅) · 𝑏) = 𝑏)
5048, 49opeq12d 4905 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩ = ⟨𝑎, 𝑏⟩)
5150eceq1d 8803 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩] = [⟨𝑎, 𝑏⟩] )
528ad4antr 731 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑅 ∈ CRing)
5322ad4antr 731 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (0g𝑅) ∈ 𝐵)
5437, 25syl 17 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (1r𝑅) ∈ 𝑆)
551, 3, 45, 6, 7, 52, 37, 53, 42, 54, 39, 19rlocaddval 33240 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(((0g𝑅) · 𝑏)(+g𝑅)(𝑎 · (1r𝑅))), ((1r𝑅) · 𝑏)⟩] )
5651, 55, 343eqtr4d 2790 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = 𝑥)
5735, 56eqtrd 2780 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
58 simpr 484 . . . . . . 7 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
5958elrlocbasi 33238 . . . . . 6 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
6057, 59r19.29vva 3222 . . . . 5 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
6133, 60syldan 590 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐿)) → ([⟨(0g𝑅), (1r𝑅)⟩] (+g𝐿)𝑥) = 𝑥)
62 rlocaddval.3 . . . . . . . 8 + = (+g𝑅)
631, 3, 62, 6, 7, 52, 37, 42, 53, 39, 54, 19rlocaddval 33240 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
6434oveq1d 7463 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ))
6543, 41oveq12d 7466 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)) = (𝑎 + (0g𝑅)))
661, 62, 2, 46, 42grpridd 19010 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑎 + (0g𝑅)) = 𝑎)
6765, 66eqtr2d 2781 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎 = ((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)))
681, 3, 23, 36, 40ringridmd 20296 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · (1r𝑅)) = 𝑏)
6968eqcomd 2746 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑏 = (𝑏 · (1r𝑅)))
7067, 69opeq12d 4905 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨𝑎, 𝑏⟩ = ⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩)
7170eceq1d 8803 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨𝑎, 𝑏⟩] = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
7234, 71eqtrd 2780 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑥 = [⟨((𝑎 · (1r𝑅)) + ((0g𝑅) · 𝑏)), (𝑏 · (1r𝑅))⟩] )
7363, 64, 723eqtr4d 2790 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7473, 59r19.29vva 3222 . . . . 5 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7533, 74syldan 590 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐿)) → (𝑥(+g𝐿)[⟨(0g𝑅), (1r𝑅)⟩] ) = 𝑥)
7617, 18, 19, 31, 61, 75ismgmid2 18706 . . 3 (𝜑 → [⟨(0g𝑅), (1r𝑅)⟩] = (0g𝐿))
77 simp-4r 783 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
78 simpr 484 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑦 = [⟨𝑐, 𝑑⟩] )
7977, 78oveq12d 7466 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(+g𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ))
808ad8antr 739 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ CRing)
819ad8antr 739 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
82 simp-6r 787 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑎𝐵)
83 simpllr 775 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑐𝐵)
84 simp-5r 785 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑏𝑆)
85 simplr 768 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑑𝑆)
861, 3, 62, 6, 7, 80, 81, 82, 83, 84, 85, 19rlocaddval 33240 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] )
8780crnggrpd 20274 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ Grp)
8820ad8antr 739 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑅 ∈ Ring)
8981, 12syl 17 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑆𝐵)
9089, 85sseldd 4009 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑑𝐵)
911, 3, 88, 82, 90ringcld 20286 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑑) ∈ 𝐵)
9289, 84sseldd 4009 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑏𝐵)
931, 3, 88, 83, 92ringcld 20286 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑐 · 𝑏) ∈ 𝐵)
941, 62, 87, 91, 93grpcld 18987 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ 𝐵)
9510, 3mgpplusg 20165 . . . . . . . . . . . 12 · = (+g‘(mulGrp‘𝑅))
9695, 81, 84, 85submcld 33021 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑏 · 𝑑) ∈ 𝑆)
9794, 96opelxpd 5739 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆))
9828ecelqsi 8831 . . . . . . . . . 10 (⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆) → [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
9997, 98syl 17 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
10086, 99eqeltrd 2844 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) ∈ ((𝐵 × 𝑆) / ))
10179, 100eqeltrd 2844 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
102 simp-4r 783 . . . . . . . 8 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
103102elrlocbasi 33238 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑐𝐵𝑑𝑆 𝑦 = [⟨𝑐, 𝑑⟩] )
104101, 103r19.29vva 3222 . . . . . 6 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
105 simplr 768 . . . . . . 7 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
106105elrlocbasi 33238 . . . . . 6 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
107104, 106r19.29vva 3222 . . . . 5 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
1081073impa 1110 . . . 4 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(+g𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
1098ad10antr 743 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ CRing)
110109crnggrpd 20274 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ Grp)
11120ad10antr 743 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑅 ∈ Ring)
112 simp-9r 793 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑎𝐵)
1139ad10antr 743 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
114113, 12syl 17 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑆𝐵)
115 simp-5r 785 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑑𝑆)
116114, 115sseldd 4009 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑑𝐵)
1171, 3, 111, 112, 116ringcld 20286 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑑) ∈ 𝐵)
118 simplr 768 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑓𝑆)
119114, 118sseldd 4009 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑓𝐵)
1201, 3, 111, 117, 119ringcld 20286 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑓) ∈ 𝐵)
121 simp-6r 787 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑐𝐵)
122 simp-8r 791 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑏𝑆)
123114, 122sseldd 4009 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑏𝐵)
1241, 3, 111, 121, 123ringcld 20286 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑏) ∈ 𝐵)
1251, 3, 111, 124, 119ringcld 20286 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑓) ∈ 𝐵)
126 simpllr 775 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑒𝐵)
1271, 3, 111, 123, 116ringcld 20286 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) ∈ 𝐵)
1281, 3, 111, 126, 127ringcld 20286 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) ∈ 𝐵)
1291, 62, 110, 120, 125, 128grpassd 18985 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))) = (((𝑎 · 𝑑) · 𝑓) + (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑)))))
1301, 3, 111, 112, 116, 119ringassd 20284 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑓) = (𝑎 · (𝑑 · 𝑓)))
1311, 3, 109, 121, 123, 119cringmul32d 33208 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑓) = ((𝑐 · 𝑓) · 𝑏))
1321, 3, 109, 126, 123, 116crng12d 20285 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) = (𝑏 · (𝑒 · 𝑑)))
1331, 3, 111, 126, 116ringcld 20286 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · 𝑑) ∈ 𝐵)
1341, 3, 109, 123, 133crngcomd 20282 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑒 · 𝑑)) = ((𝑒 · 𝑑) · 𝑏))
135132, 134eqtrd 2780 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑒 · (𝑏 · 𝑑)) = ((𝑒 · 𝑑) · 𝑏))
136131, 135oveq12d 7466 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏)))
137130, 136oveq12d 7466 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑓) + (((𝑐 · 𝑏) · 𝑓) + (𝑒 · (𝑏 · 𝑑)))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
138129, 137eqtrd 2780 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
1391, 62, 3, 111, 117, 124, 119ringdird 33210 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) = (((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)))
140139oveq1d 7463 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = ((((𝑎 · 𝑑) · 𝑓) + ((𝑐 · 𝑏) · 𝑓)) + (𝑒 · (𝑏 · 𝑑))))
1411, 3, 111, 121, 119ringcld 20286 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑓) ∈ 𝐵)
1421, 62, 3, 111, 141, 133, 123ringdird 33210 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏) = (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏)))
143142oveq2d 7464 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) · 𝑏) + ((𝑒 · 𝑑) · 𝑏))))
144138, 140, 1433eqtr4d 2790 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))) = ((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)))
1451, 3, 111, 123, 116, 119ringassd 20284 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = (𝑏 · (𝑑 · 𝑓)))
146144, 145opeq12d 4905 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩)
147146eceq1d 8803 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩] )
1481, 62, 110, 117, 124grpcld 18987 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ 𝐵)
14995, 113, 122, 115submcld 33021 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) ∈ 𝑆)
1501, 3, 62, 6, 7, 109, 113, 148, 126, 149, 118, 19rlocaddval 33240 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑓) + (𝑒 · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · 𝑓)⟩] )
1511, 62, 110, 141, 133grpcld 18987 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑓) + (𝑒 · 𝑑)) ∈ 𝐵)
15295, 113, 115, 118submcld 33021 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑑 · 𝑓) ∈ 𝑆)
1531, 3, 62, 6, 7, 109, 113, 112, 151, 122, 152, 19rlocaddval 33240 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = [⟨((𝑎 · (𝑑 · 𝑓)) + (((𝑐 · 𝑓) + (𝑒 · 𝑑)) · 𝑏)), (𝑏 · (𝑑 · 𝑓))⟩] )
154147, 150, 1533eqtr4d 2790 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
1551, 3, 62, 6, 7, 109, 113, 112, 121, 122, 115, 19rlocaddval 33240 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] )
156155oveq1d 7463 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ))
1571, 3, 62, 6, 7, 109, 113, 121, 126, 115, 118, 19rlocaddval 33240 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] )
158157oveq2d 7464 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
159154, 156, 1583eqtr4d 2790 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
160 simp-7r 789 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
161 simp-4r 783 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑦 = [⟨𝑐, 𝑑⟩] )
162160, 161oveq12d 7466 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(+g𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] ))
163 simpr 484 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → 𝑧 = [⟨𝑒, 𝑓⟩] )
164162, 163oveq12d 7466 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)[⟨𝑒, 𝑓⟩] ))
165161, 163oveq12d 7466 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑦(+g𝐿)𝑧) = ([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] ))
166160, 165oveq12d 7466 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (+g𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
167159, 164, 1663eqtr4d 2790 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
168 simpr3 1196 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑧 ∈ ((𝐵 × 𝑆) / ))
169168ad6antr 735 . . . . . . . 8 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → 𝑧 ∈ ((𝐵 × 𝑆) / ))
170169elrlocbasi 33238 . . . . . . 7 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ∃𝑒𝐵𝑓𝑆 𝑧 = [⟨𝑒, 𝑓⟩] )
171167, 170r19.29vva 3222 . . . . . 6 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
172 simpr2 1195 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
173172ad5ant12 755 . . . . . . 7 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑦 ∈ ((𝐵 × 𝑆) / ))
174173elrlocbasi 33238 . . . . . 6 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑐𝐵𝑑𝑆 𝑦 = [⟨𝑐, 𝑑⟩] )
175171, 174r19.29vva 3222 . . . . 5 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
176 simpr1 1194 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → 𝑥 ∈ ((𝐵 × 𝑆) / ))
177176elrlocbasi 33238 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ∃𝑎𝐵𝑏𝑆 𝑥 = [⟨𝑎, 𝑏⟩] )
178175, 177r19.29vva 3222 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(+g𝐿)𝑦)(+g𝐿)𝑧) = (𝑥(+g𝐿)(𝑦(+g𝐿)𝑧)))
17914, 15, 108, 178, 30, 60, 74ismndd 18794 . . 3 (𝜑𝐿 ∈ Mnd)
180 eqid 2740 . . . . . . . 8 (invg𝑅) = (invg𝑅)
1811, 180, 46, 42grpinvcld 19028 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((invg𝑅)‘𝑎) ∈ 𝐵)
182181, 39opelxpd 5739 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((invg𝑅)‘𝑎), 𝑏⟩ ∈ (𝐵 × 𝑆))
18328ecelqsi 8831 . . . . . 6 (⟨((invg𝑅)‘𝑎), 𝑏⟩ ∈ (𝐵 × 𝑆) → [⟨((invg𝑅)‘𝑎), 𝑏⟩] ∈ ((𝐵 × 𝑆) / ))
184182, 183syl 17 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((invg𝑅)‘𝑎), 𝑏⟩] ∈ ((𝐵 × 𝑆) / ))
185 simpr 484 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] )
186 simplr 768 . . . . . . 7 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → 𝑥 = [⟨𝑎, 𝑏⟩] )
187185, 186oveq12d 7466 . . . . . 6 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → (𝑢(+g𝐿)𝑥) = ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ))
188187eqeq1d 2742 . . . . 5 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑢 = [⟨((invg𝑅)‘𝑎), 𝑏⟩] ) → ((𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] ↔ ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(0g𝑅), (1r𝑅)⟩] ))
1891, 3, 62, 6, 7, 52, 37, 181, 42, 39, 39, 19rlocaddval 33240 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩] )
1901, 62, 2, 180, 46, 42grplinvd 19034 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((invg𝑅)‘𝑎) + 𝑎) = (0g𝑅))
191190oveq1d 7463 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) + 𝑎) · 𝑏) = ((0g𝑅) · 𝑏))
1921, 62, 3, 36, 181, 42, 40ringdird 33210 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) + 𝑎) · 𝑏) = ((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)))
193191, 192, 413eqtr3d 2788 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)) = (0g𝑅))
194193opeq1d 4903 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩ = ⟨(0g𝑅), (𝑏 · 𝑏)⟩)
195194eceq1d 8803 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((((invg𝑅)‘𝑎) · 𝑏) + (𝑎 · 𝑏)), (𝑏 · 𝑏)⟩] = [⟨(0g𝑅), (𝑏 · 𝑏)⟩] )
1961, 2, 23, 3, 4, 5, 7, 8, 9erler 33237 . . . . . . . 8 (𝜑 Er (𝐵 × 𝑆))
197196ad4antr 731 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → Er (𝐵 × 𝑆))
198 eqidd 2741 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (𝑏 · 𝑏)⟩ = ⟨(0g𝑅), (𝑏 · 𝑏)⟩)
199 eqidd 2741 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (1r𝑅)⟩ = ⟨(0g𝑅), (1r𝑅)⟩)
20095, 37, 39, 39submcld 33021 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · 𝑏) ∈ 𝑆)
2011, 3, 23, 36, 53ringridmd 20296 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · (1r𝑅)) = (0g𝑅))
20238, 200sseldd 4009 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑏 · 𝑏) ∈ 𝐵)
2031, 3, 2, 36, 202ringlzd 20318 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅) · (𝑏 · 𝑏)) = (0g𝑅))
204201, 203oveq12d 7466 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏))) = ((0g𝑅)(-g𝑅)(0g𝑅)))
2051, 2, 4grpsubid 19064 . . . . . . . . . . . 12 ((𝑅 ∈ Grp ∧ (0g𝑅) ∈ 𝐵) → ((0g𝑅)(-g𝑅)(0g𝑅)) = (0g𝑅))
20646, 53, 205syl2anc 583 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((0g𝑅)(-g𝑅)(0g𝑅)) = (0g𝑅))
207204, 206eqtrd 2780 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏))) = (0g𝑅))
208207oveq2d 7464 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏)))) = ((𝑏 · 𝑏) · (0g𝑅)))
2091, 3, 2, 36, 202ringrzd 20319 . . . . . . . . 9 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (0g𝑅)) = (0g𝑅))
210208, 209eqtrd 2780 . . . . . . . 8 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑏 · 𝑏) · (((0g𝑅) · (1r𝑅))(-g𝑅)((0g𝑅) · (𝑏 · 𝑏)))) = (0g𝑅))
2111, 7, 38, 2, 3, 4, 198, 199, 53, 53, 200, 54, 200, 210erlbrd 33235 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨(0g𝑅), (𝑏 · 𝑏)⟩ ⟨(0g𝑅), (1r𝑅)⟩)
212197, 211erthi 8816 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨(0g𝑅), (𝑏 · 𝑏)⟩] = [⟨(0g𝑅), (1r𝑅)⟩] )
213189, 195, 2123eqtrd 2784 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨((invg𝑅)‘𝑎), 𝑏⟩] (+g𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(0g𝑅), (1r𝑅)⟩] )
214184, 188, 213rspcedvd 3637 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ∃𝑢 ∈ ((𝐵 × 𝑆) / )(𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] )
215214, 59r19.29vva 3222 . . 3 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ∃𝑢 ∈ ((𝐵 × 𝑆) / )(𝑢(+g𝐿)𝑥) = [⟨(0g𝑅), (1r𝑅)⟩] )
21614, 15, 76, 179, 215isgrpd2e 18995 . 2 (𝜑𝐿 ∈ Grp)
21777, 78oveq12d 7466 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ))
218 eqid 2740 . . . . . . . 8 (.r𝐿) = (.r𝐿)
2191, 3, 62, 6, 7, 80, 81, 82, 83, 84, 85, 218rlocmulval 33241 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] )
2201, 3, 88, 82, 83ringcld 20286 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑐) ∈ 𝐵)
221220, 96opelxpd 5739 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆))
22228ecelqsi 8831 . . . . . . . 8 (⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ ∈ (𝐵 × 𝑆) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
223221, 222syl 17 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] ∈ ((𝐵 × 𝑆) / ))
224219, 223eqeltrd 2844 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) ∈ ((𝐵 × 𝑆) / ))
225217, 224eqeltrd 2844 . . . . 5 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
226225, 103r19.29vva 3222 . . . 4 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
227226, 106r19.29vva 3222 . . 3 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
2282273impa 1110 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) ∈ ((𝐵 × 𝑆) / ))
2291, 3, 111, 112, 121, 126ringassd 20284 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑐) · 𝑒) = (𝑎 · (𝑐 · 𝑒)))
230229, 145opeq12d 4905 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩)
231230eceq1d 8803 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩] )
2321, 3, 111, 112, 121ringcld 20286 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑐) ∈ 𝐵)
2331, 3, 62, 6, 7, 109, 113, 232, 126, 149, 118, 218rlocmulval 33241 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨((𝑎 · 𝑐) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] )
2341, 3, 111, 121, 126ringcld 20286 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑐 · 𝑒) ∈ 𝐵)
2351, 3, 62, 6, 7, 109, 113, 112, 234, 122, 152, 218rlocmulval 33241 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ) = [⟨(𝑎 · (𝑐 · 𝑒)), (𝑏 · (𝑑 · 𝑓))⟩] )
236231, 233, 2353eqtr4d 2790 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
2371, 3, 62, 6, 7, 109, 113, 112, 121, 122, 115, 218rlocmulval 33241 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] )
238237oveq1d 7463 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
2391, 3, 62, 6, 7, 109, 113, 121, 126, 115, 118, 218rlocmulval 33241 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] )
240239oveq2d 7464 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
241236, 238, 2403eqtr4d 2790 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
242160, 161oveq12d 7466 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)𝑦) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ))
243242, 163oveq12d 7466 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ))
244161, 163oveq12d 7466 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑦(.r𝐿)𝑧) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
245160, 244oveq12d 7466 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
246241, 243, 2453eqtr4d 2790 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
247246, 170r19.29vva 3222 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
248247, 174r19.29vva 3222 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
249248, 177r19.29vva 3222 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(.r𝐿)𝑦)(.r𝐿)𝑧) = (𝑥(.r𝐿)(𝑦(.r𝐿)𝑧)))
250196ad10antr 743 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → Er (𝐵 × 𝑆))
251 eqidd 2741 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩ = ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩)
2521, 3, 111, 112, 123ringcld 20286 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑏) ∈ 𝐵)
2531, 62, 3, 111, 252, 141, 133ringdid 33209 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑏) · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) = (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))))
2541, 3, 111, 112, 123, 151ringassd 20284 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑏) · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
255253, 254eqtr3d 2782 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
25610crngmgp 20268 . . . . . . . . . . . . . . . 16 (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
2578, 256syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
258257ad10antr 743 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (mulGrp‘𝑅) ∈ CMnd)
25911, 95, 258, 112, 121, 123, 119cmn4d 33018 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑐) · (𝑏 · 𝑓)) = ((𝑎 · 𝑏) · (𝑐 · 𝑓)))
26011, 95, 258, 112, 126, 123, 116cmn4d 33018 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑏 · 𝑑)) = ((𝑎 · 𝑏) · (𝑒 · 𝑑)))
261259, 260oveq12d 7466 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))) = (((𝑎 · 𝑏) · (𝑐 · 𝑓)) + ((𝑎 · 𝑏) · (𝑒 · 𝑑))))
2621, 3, 109, 123, 112, 151crng12d 20285 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) = (𝑎 · (𝑏 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
263255, 261, 2623eqtr4d 2790 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))) = (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
2641, 3, 109, 127, 123, 119crng12d 20285 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · (𝑏 · 𝑓)) = (𝑏 · ((𝑏 · 𝑑) · 𝑓)))
265145oveq2d 7464 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · ((𝑏 · 𝑑) · 𝑓)) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
266264, 265eqtrd 2780 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · (𝑏 · 𝑓)) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
267263, 266opeq12d 4905 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩ = ⟨(𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))), (𝑏 · (𝑏 · (𝑑 · 𝑓)))⟩)
2681, 3, 111, 112, 151ringcld 20286 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))) ∈ 𝐵)
2691, 3, 111, 123, 268ringcld 20286 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) ∈ 𝐵)
27095, 113, 122, 152submcld 33021 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑑 · 𝑓)) ∈ 𝑆)
27195, 113, 122, 270submcld 33021 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑏 · (𝑑 · 𝑓))) ∈ 𝑆)
272 eqidd 2741 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))) = (𝑏 · (𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑)))))
273 eqidd 2741 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · (𝑏 · (𝑑 · 𝑓))) = (𝑏 · (𝑏 · (𝑑 · 𝑓))))
2741, 7, 109, 113, 3, 251, 267, 268, 269, 270, 271, 122, 272, 273erlbr2d 33236 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩ ⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩)
275250, 274erthi 8816 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩] = [⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩] )
2761, 3, 62, 6, 7, 109, 113, 112, 151, 122, 152, 218rlocmulval 33241 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = [⟨(𝑎 · ((𝑐 · 𝑓) + (𝑒 · 𝑑))), (𝑏 · (𝑑 · 𝑓))⟩] )
2771, 3, 111, 112, 126ringcld 20286 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑎 · 𝑒) ∈ 𝐵)
27895, 113, 122, 118submcld 33021 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑓) ∈ 𝑆)
2791, 3, 62, 6, 7, 109, 113, 232, 277, 149, 278, 19rlocaddval 33240 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ) = [⟨(((𝑎 · 𝑐) · (𝑏 · 𝑓)) + ((𝑎 · 𝑒) · (𝑏 · 𝑑))), ((𝑏 · 𝑑) · (𝑏 · 𝑓))⟩] )
280275, 276, 2793eqtr4d 2790 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ))
281157oveq2d 7464 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨((𝑐 · 𝑓) + (𝑒 · 𝑑)), (𝑑 · 𝑓)⟩] ))
2821, 3, 62, 6, 7, 109, 113, 112, 126, 122, 118, 218rlocmulval 33241 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] )
283237, 282oveq12d 7466 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] (+g𝐿)[⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] ))
284280, 281, 2833eqtr4d 2790 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
285160, 165oveq12d 7466 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ([⟨𝑎, 𝑏⟩] (.r𝐿)([⟨𝑐, 𝑑⟩] (+g𝐿)[⟨𝑒, 𝑓⟩] )))
286160, 163oveq12d 7466 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)𝑧) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
287242, 286oveq12d 7466 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] )(+g𝐿)([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
288284, 285, 2873eqtr4d 2790 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
289288, 170r19.29vva 3222 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
290289, 174r19.29vva 3222 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
291290, 177r19.29vva 3222 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → (𝑥(.r𝐿)(𝑦(+g𝐿)𝑧)) = ((𝑥(.r𝐿)𝑦)(+g𝐿)(𝑥(.r𝐿)𝑧)))
2921, 62, 3, 111, 117, 124, 126ringdird 33210 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒) = (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)))
293292opeq1d 4903 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ = ⟨(((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)), ((𝑏 · 𝑑) · 𝑓)⟩)
2941, 3, 111, 117, 126, 119ringassd 20284 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑒) · 𝑓) = ((𝑎 · 𝑑) · (𝑒 · 𝑓)))
2951, 3, 111, 117, 126ringcld 20286 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑑) · 𝑒) ∈ 𝐵)
2961, 3, 109, 119, 295crngcomd 20282 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · ((𝑎 · 𝑑) · 𝑒)) = (((𝑎 · 𝑑) · 𝑒) · 𝑓))
29711, 95, 258, 112, 126, 116, 119cmn4d 33018 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑑 · 𝑓)) = ((𝑎 · 𝑑) · (𝑒 · 𝑓)))
298294, 296, 2973eqtr4rd 2791 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑎 · 𝑒) · (𝑑 · 𝑓)) = (𝑓 · ((𝑎 · 𝑑) · 𝑒)))
2991, 3, 111, 124, 126, 119ringassd 20284 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑐 · 𝑏) · 𝑒) · 𝑓) = ((𝑐 · 𝑏) · (𝑒 · 𝑓)))
3001, 3, 111, 124, 126ringcld 20286 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑏) · 𝑒) ∈ 𝐵)
3011, 3, 109, 119, 300crngcomd 20282 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · ((𝑐 · 𝑏) · 𝑒)) = (((𝑐 · 𝑏) · 𝑒) · 𝑓))
30211, 95, 258, 121, 126, 123, 119cmn4d 33018 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑒) · (𝑏 · 𝑓)) = ((𝑐 · 𝑏) · (𝑒 · 𝑓)))
303299, 301, 3023eqtr4rd 2791 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑐 · 𝑒) · (𝑏 · 𝑓)) = (𝑓 · ((𝑐 · 𝑏) · 𝑒)))
304298, 303oveq12d 7466 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))) = ((𝑓 · ((𝑎 · 𝑑) · 𝑒)) + (𝑓 · ((𝑐 · 𝑏) · 𝑒))))
3051, 62, 3, 111, 119, 295, 300ringdid 33209 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) = ((𝑓 · ((𝑎 · 𝑑) · 𝑒)) + (𝑓 · ((𝑐 · 𝑏) · 𝑒))))
306304, 305eqtr4d 2783 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))) = (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))))
307114, 278sseldd 4009 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑓) ∈ 𝐵)
3081, 3, 111, 116, 307, 119ringassd 20284 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑑 · (𝑏 · 𝑓)) · 𝑓) = (𝑑 · ((𝑏 · 𝑓) · 𝑓)))
3091, 3, 109, 123, 116crngcomd 20282 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑏 · 𝑑) = (𝑑 · 𝑏))
310309oveq1d 7463 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = ((𝑑 · 𝑏) · 𝑓))
3111, 3, 111, 116, 123, 119ringassd 20284 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑑 · 𝑏) · 𝑓) = (𝑑 · (𝑏 · 𝑓)))
312310, 311eqtrd 2780 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) = (𝑑 · (𝑏 · 𝑓)))
313312oveq1d 7463 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) = ((𝑑 · (𝑏 · 𝑓)) · 𝑓))
3141, 3, 109, 307, 116, 119crng12d 20285 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑓) · (𝑑 · 𝑓)) = (𝑑 · ((𝑏 · 𝑓) · 𝑓)))
315308, 313, 3143eqtr4rd 2791 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑓) · (𝑑 · 𝑓)) = (((𝑏 · 𝑑) · 𝑓) · 𝑓))
316306, 315opeq12d 4905 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩ = ⟨(𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))), (((𝑏 · 𝑑) · 𝑓) · 𝑓)⟩)
3171, 62, 110, 295, 300grpcld 18987 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒)) ∈ 𝐵)
3181, 3, 111, 119, 317ringcld 20286 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) ∈ 𝐵)
319145, 270eqeltrd 2844 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) ∈ 𝑆)
32095, 113, 319, 118submcld 33021 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) ∈ 𝑆)
321 eqidd 2741 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))) = (𝑓 · (((𝑎 · 𝑑) · 𝑒) + ((𝑐 · 𝑏) · 𝑒))))
322114, 319sseldd 4009 . . . . . . . . . . 11 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑏 · 𝑑) · 𝑓) ∈ 𝐵)
3231, 3, 109, 322, 119crngcomd 20282 . . . . . . . . . 10 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (((𝑏 · 𝑑) · 𝑓) · 𝑓) = (𝑓 · ((𝑏 · 𝑑) · 𝑓)))
3241, 7, 109, 113, 3, 293, 316, 317, 318, 319, 320, 118, 321, 323erlbr2d 33236 . . . . . . . . 9 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩ ⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩)
325250, 324erthi 8816 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → [⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] = [⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩] )
3261, 3, 62, 6, 7, 109, 113, 148, 126, 149, 118, 218rlocmulval 33241 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = [⟨(((𝑎 · 𝑑) + (𝑐 · 𝑏)) · 𝑒), ((𝑏 · 𝑑) · 𝑓)⟩] )
3271, 3, 62, 6, 7, 109, 113, 277, 234, 278, 152, 19rlocaddval 33240 . . . . . . . 8 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ) = [⟨(((𝑎 · 𝑒) · (𝑑 · 𝑓)) + ((𝑐 · 𝑒) · (𝑏 · 𝑓))), ((𝑏 · 𝑓) · (𝑑 · 𝑓))⟩] )
328325, 326, 3273eqtr4d 2790 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
329155oveq1d 7463 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = ([⟨((𝑎 · 𝑑) + (𝑐 · 𝑏)), (𝑏 · 𝑑)⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] ))
330282, 239oveq12d 7466 . . . . . . 7 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )) = ([⟨(𝑎 · 𝑒), (𝑏 · 𝑓)⟩] (+g𝐿)[⟨(𝑐 · 𝑒), (𝑑 · 𝑓)⟩] ))
331328, 329, 3303eqtr4d 2790 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
332162, 163oveq12d 7466 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = (([⟨𝑎, 𝑏⟩] (+g𝐿)[⟨𝑐, 𝑑⟩] )(.r𝐿)[⟨𝑒, 𝑓⟩] ))
333286, 244oveq12d 7466 . . . . . 6 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)) = (([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )(+g𝐿)([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑒, 𝑓⟩] )))
334331, 332, 3333eqtr4d 2790 . . . . 5 (((((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) ∧ 𝑒𝐵) ∧ 𝑓𝑆) ∧ 𝑧 = [⟨𝑒, 𝑓⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
335334, 170r19.29vva 3222 . . . 4 ((((((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
336335, 174r19.29vva 3222 . . 3 (((((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
337336, 177r19.29vva 3222 . 2 ((𝜑 ∧ (𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑧 ∈ ((𝐵 × 𝑆) / ))) → ((𝑥(+g𝐿)𝑦)(.r𝐿)𝑧) = ((𝑥(.r𝐿)𝑧)(+g𝐿)(𝑦(.r𝐿)𝑧)))
33813, 26sseldd 4009 . . . 4 (𝜑 → (1r𝑅) ∈ 𝐵)
339338, 26opelxpd 5739 . . 3 (𝜑 → ⟨(1r𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆))
34028ecelqsi 8831 . . 3 (⟨(1r𝑅), (1r𝑅)⟩ ∈ (𝐵 × 𝑆) → [⟨(1r𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
341339, 340syl 17 . 2 (𝜑 → [⟨(1r𝑅), (1r𝑅)⟩] ∈ ((𝐵 × 𝑆) / ))
34234oveq2d 7464 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
3431, 3, 23, 36, 42ringlidmd 20295 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ((1r𝑅) · 𝑎) = 𝑎)
344343, 49opeq12d 4905 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩ = ⟨𝑎, 𝑏⟩)
345344eceq1d 8803 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩] = [⟨𝑎, 𝑏⟩] )
34638, 54sseldd 4009 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (1r𝑅) ∈ 𝐵)
3471, 3, 62, 6, 7, 52, 37, 346, 42, 54, 39, 218rlocmulval 33241 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨((1r𝑅) · 𝑎), ((1r𝑅) · 𝑏)⟩] )
348345, 347, 343eqtr4d 2790 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = 𝑥)
349342, 348eqtrd 2780 . . 3 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = 𝑥)
350349, 59r19.29vva 3222 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → ([⟨(1r𝑅), (1r𝑅)⟩] (.r𝐿)𝑥) = 𝑥)
3511, 3, 62, 6, 7, 52, 37, 42, 346, 39, 54, 218rlocmulval 33241 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = [⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩] )
35234oveq1d 7463 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ))
35343eqcomd 2746 . . . . . . 7 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → 𝑎 = (𝑎 · (1r𝑅)))
354353, 69opeq12d 4905 . . . . . 6 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → ⟨𝑎, 𝑏⟩ = ⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩)
355354eceq1d 8803 . . . . 5 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → [⟨𝑎, 𝑏⟩] = [⟨(𝑎 · (1r𝑅)), (𝑏 · (1r𝑅))⟩] )
356351, 352, 3553eqtr4d 2790 . . . 4 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = [⟨𝑎, 𝑏⟩] )
357356, 34eqtr4d 2783 . . 3 (((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = 𝑥)
358357, 59r19.29vva 3222 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)[⟨(1r𝑅), (1r𝑅)⟩] ) = 𝑥)
3591, 3, 80, 82, 83crngcomd 20282 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑎 · 𝑐) = (𝑐 · 𝑎))
3601, 3, 80, 92, 90crngcomd 20282 . . . . . . . . 9 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑏 · 𝑑) = (𝑑 · 𝑏))
361359, 360opeq12d 4905 . . . . . . . 8 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩ = ⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩)
362361eceq1d 8803 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → [⟨(𝑎 · 𝑐), (𝑏 · 𝑑)⟩] = [⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩] )
3631, 3, 62, 6, 7, 80, 81, 83, 82, 85, 84, 218rlocmulval 33241 . . . . . . 7 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ) = [⟨(𝑐 · 𝑎), (𝑑 · 𝑏)⟩] )
364362, 219, 3633eqtr4d 2790 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → ([⟨𝑎, 𝑏⟩] (.r𝐿)[⟨𝑐, 𝑑⟩] ) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
36578, 77oveq12d 7466 . . . . . 6 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑦(.r𝐿)𝑥) = ([⟨𝑐, 𝑑⟩] (.r𝐿)[⟨𝑎, 𝑏⟩] ))
366364, 217, 3653eqtr4d 2790 . . . . 5 (((((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) ∧ 𝑐𝐵) ∧ 𝑑𝑆) ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
367366, 103r19.29vva 3222 . . . 4 ((((((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑎𝐵) ∧ 𝑏𝑆) ∧ 𝑥 = [⟨𝑎, 𝑏⟩] ) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
368367, 106r19.29vva 3222 . . 3 (((𝜑𝑥 ∈ ((𝐵 × 𝑆) / )) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
3693683impa 1110 . 2 ((𝜑𝑥 ∈ ((𝐵 × 𝑆) / ) ∧ 𝑦 ∈ ((𝐵 × 𝑆) / )) → (𝑥(.r𝐿)𝑦) = (𝑦(.r𝐿)𝑥))
37014, 15, 16, 216, 228, 249, 291, 337, 341, 350, 358, 369iscrngd 20315 1 (𝜑𝐿 ∈ CRing)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1537  wcel 2108  wrex 3076  wss 3976  cop 4654   × cxp 5698  cfv 6573  (class class class)co 7448   Er wer 8760  [cec 8761   / cqs 8762  Basecbs 17258  +gcplusg 17311  .rcmulr 17312  0gc0g 17499  SubMndcsubmnd 18817  Grpcgrp 18973  invgcminusg 18974  -gcsg 18975  CMndccmn 19822  mulGrpcmgp 20161  1rcur 20208  Ringcrg 20260  CRingccrg 20261   ~RL cerl 33225   RLocal crloc 33226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-er 8763  df-ec 8765  df-qs 8769  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-sup 9511  df-inf 9512  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-z 12640  df-dec 12759  df-uz 12904  df-fz 13568  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-sca 17327  df-vsca 17328  df-ip 17329  df-tset 17330  df-ple 17331  df-ds 17333  df-0g 17501  df-imas 17568  df-qus 17569  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-submnd 18819  df-grp 18976  df-minusg 18977  df-sbg 18978  df-cmn 19824  df-abl 19825  df-mgp 20162  df-rng 20180  df-ur 20209  df-ring 20262  df-cring 20263  df-erl 33227  df-rloc 33228
This theorem is referenced by:  rloc0g  33243  rloc1r  33244  rlocf1  33245  fracfld  33275
  Copyright terms: Public domain W3C validator