MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsrmo Structured version   Visualization version   GIF version

Theorem mulsrmo 11105
Description: There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
Assertion
Ref Expression
mulsrmo ((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โ†’ โˆƒ*๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ))
Distinct variable groups:   ๐‘ก,๐ด,๐‘ข,๐‘ฃ,๐‘ค,๐‘ง   ๐‘ก,๐ต,๐‘ข,๐‘ฃ,๐‘ค,๐‘ง

Proof of Theorem mulsrmo
Dummy variables ๐‘“ ๐‘” โ„Ž ๐‘ž ๐‘  are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 enrer 11094 . . . . . . . . . . . . . . . 16 ~R Er (P ร— P)
21a1i 11 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โˆง ((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง (๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ))) โ†’ ~R Er (P ร— P))
3 prsrlem1 11103 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โˆง ((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง (๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ))) โ†’ ((((๐‘ค โˆˆ P โˆง ๐‘ฃ โˆˆ P) โˆง (๐‘  โˆˆ P โˆง ๐‘“ โˆˆ P)) โˆง ((๐‘ข โˆˆ P โˆง ๐‘ก โˆˆ P) โˆง (๐‘” โˆˆ P โˆง โ„Ž โˆˆ P))) โˆง ((๐‘ค +P ๐‘“) = (๐‘ฃ +P ๐‘ ) โˆง (๐‘ข +P โ„Ž) = (๐‘ก +P ๐‘”))))
4 mulcmpblnr 11102 . . . . . . . . . . . . . . . . 17 ((((๐‘ค โˆˆ P โˆง ๐‘ฃ โˆˆ P) โˆง (๐‘  โˆˆ P โˆง ๐‘“ โˆˆ P)) โˆง ((๐‘ข โˆˆ P โˆง ๐‘ก โˆˆ P) โˆง (๐‘” โˆˆ P โˆง โ„Ž โˆˆ P))) โ†’ (((๐‘ค +P ๐‘“) = (๐‘ฃ +P ๐‘ ) โˆง (๐‘ข +P โ„Ž) = (๐‘ก +P ๐‘”)) โ†’ โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ ~R โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ))
54imp 405 . . . . . . . . . . . . . . . 16 (((((๐‘ค โˆˆ P โˆง ๐‘ฃ โˆˆ P) โˆง (๐‘  โˆˆ P โˆง ๐‘“ โˆˆ P)) โˆง ((๐‘ข โˆˆ P โˆง ๐‘ก โˆˆ P) โˆง (๐‘” โˆˆ P โˆง โ„Ž โˆˆ P))) โˆง ((๐‘ค +P ๐‘“) = (๐‘ฃ +P ๐‘ ) โˆง (๐‘ข +P โ„Ž) = (๐‘ก +P ๐‘”))) โ†’ โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ ~R โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ)
63, 5syl 17 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โˆง ((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง (๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ))) โ†’ โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ ~R โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ)
72, 6erthi 8783 . . . . . . . . . . . . . 14 (((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โˆง ((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง (๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ))) โ†’ [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R )
87adantrlr 721 . . . . . . . . . . . . 13 (((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โˆง (((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง (๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ))) โ†’ [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R )
98adantrrr 723 . . . . . . . . . . . 12 (((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โˆง (((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง ((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R ))) โ†’ [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R )
10 simprlr 778 . . . . . . . . . . . 12 (((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โˆง (((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง ((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R ))) โ†’ ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R )
11 simprrr 780 . . . . . . . . . . . 12 (((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โˆง (((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง ((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R ))) โ†’ ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R )
129, 10, 113eqtr4d 2778 . . . . . . . . . . 11 (((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โˆง (((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง ((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R ))) โ†’ ๐‘ง = ๐‘ž)
1312expr 455 . . . . . . . . . 10 (((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โˆง ((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R )) โ†’ (((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R ) โ†’ ๐‘ง = ๐‘ž))
1413exlimdvv 1929 . . . . . . . . 9 (((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โˆง ((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R )) โ†’ (โˆƒ๐‘”โˆƒโ„Ž((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R ) โ†’ ๐‘ง = ๐‘ž))
1514exlimdvv 1929 . . . . . . . 8 (((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โˆง ((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R )) โ†’ (โˆƒ๐‘ โˆƒ๐‘“โˆƒ๐‘”โˆƒโ„Ž((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R ) โ†’ ๐‘ง = ๐‘ž))
1615ex 411 . . . . . . 7 ((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โ†’ (((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โ†’ (โˆƒ๐‘ โˆƒ๐‘“โˆƒ๐‘”โˆƒโ„Ž((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R ) โ†’ ๐‘ง = ๐‘ž)))
1716exlimdvv 1929 . . . . . 6 ((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โ†’ (โˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โ†’ (โˆƒ๐‘ โˆƒ๐‘“โˆƒ๐‘”โˆƒโ„Ž((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R ) โ†’ ๐‘ง = ๐‘ž)))
1817exlimdvv 1929 . . . . 5 ((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โ†’ (โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โ†’ (โˆƒ๐‘ โˆƒ๐‘“โˆƒ๐‘”โˆƒโ„Ž((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R ) โ†’ ๐‘ง = ๐‘ž)))
1918impd 409 . . . 4 ((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โ†’ ((โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง โˆƒ๐‘ โˆƒ๐‘“โˆƒ๐‘”โˆƒโ„Ž((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R )) โ†’ ๐‘ง = ๐‘ž))
2019alrimivv 1923 . . 3 ((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โ†’ โˆ€๐‘งโˆ€๐‘ž((โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง โˆƒ๐‘ โˆƒ๐‘“โˆƒ๐‘”โˆƒโ„Ž((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R )) โ†’ ๐‘ง = ๐‘ž))
21 opeq12 4880 . . . . . . . . . . 11 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ โŸจ๐‘ค, ๐‘ฃโŸฉ = โŸจ๐‘ , ๐‘“โŸฉ)
2221eceq1d 8770 . . . . . . . . . 10 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R = [โŸจ๐‘ , ๐‘“โŸฉ] ~R )
2322eqeq2d 2739 . . . . . . . . 9 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ (๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โ†” ๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R ))
2423anbi1d 629 . . . . . . . 8 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ ((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โ†” (๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R )))
25 simpl 481 . . . . . . . . . . . . 13 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ ๐‘ค = ๐‘ )
2625oveq1d 7441 . . . . . . . . . . . 12 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ (๐‘ค ยทP ๐‘ข) = (๐‘  ยทP ๐‘ข))
27 simpr 483 . . . . . . . . . . . . 13 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ ๐‘ฃ = ๐‘“)
2827oveq1d 7441 . . . . . . . . . . . 12 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ (๐‘ฃ ยทP ๐‘ก) = (๐‘“ ยทP ๐‘ก))
2926, 28oveq12d 7444 . . . . . . . . . . 11 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)) = ((๐‘  ยทP ๐‘ข) +P (๐‘“ ยทP ๐‘ก)))
3025oveq1d 7441 . . . . . . . . . . . 12 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ (๐‘ค ยทP ๐‘ก) = (๐‘  ยทP ๐‘ก))
3127oveq1d 7441 . . . . . . . . . . . 12 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ (๐‘ฃ ยทP ๐‘ข) = (๐‘“ ยทP ๐‘ข))
3230, 31oveq12d 7444 . . . . . . . . . . 11 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข)) = ((๐‘  ยทP ๐‘ก) +P (๐‘“ ยทP ๐‘ข)))
3329, 32opeq12d 4886 . . . . . . . . . 10 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ = โŸจ((๐‘  ยทP ๐‘ข) +P (๐‘“ ยทP ๐‘ก)), ((๐‘  ยทP ๐‘ก) +P (๐‘“ ยทP ๐‘ข))โŸฉ)
3433eceq1d 8770 . . . . . . . . 9 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R = [โŸจ((๐‘  ยทP ๐‘ข) +P (๐‘“ ยทP ๐‘ก)), ((๐‘  ยทP ๐‘ก) +P (๐‘“ ยทP ๐‘ข))โŸฉ] ~R )
3534eqeq2d 2739 . . . . . . . 8 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ (๐‘ž = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R โ†” ๐‘ž = [โŸจ((๐‘  ยทP ๐‘ข) +P (๐‘“ ยทP ๐‘ก)), ((๐‘  ยทP ๐‘ก) +P (๐‘“ ยทP ๐‘ข))โŸฉ] ~R ))
3624, 35anbi12d 630 . . . . . . 7 ((๐‘ค = ๐‘  โˆง ๐‘ฃ = ๐‘“) โ†’ (((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โ†” ((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘ข) +P (๐‘“ ยทP ๐‘ก)), ((๐‘  ยทP ๐‘ก) +P (๐‘“ ยทP ๐‘ข))โŸฉ] ~R )))
37 opeq12 4880 . . . . . . . . . . 11 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ โŸจ๐‘ข, ๐‘กโŸฉ = โŸจ๐‘”, โ„ŽโŸฉ)
3837eceq1d 8770 . . . . . . . . . 10 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ [โŸจ๐‘ข, ๐‘กโŸฉ] ~R = [โŸจ๐‘”, โ„ŽโŸฉ] ~R )
3938eqeq2d 2739 . . . . . . . . 9 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ (๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R โ†” ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ))
4039anbi2d 628 . . . . . . . 8 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ ((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โ†” (๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R )))
41 simpl 481 . . . . . . . . . . . . 13 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ ๐‘ข = ๐‘”)
4241oveq2d 7442 . . . . . . . . . . . 12 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ (๐‘  ยทP ๐‘ข) = (๐‘  ยทP ๐‘”))
43 simpr 483 . . . . . . . . . . . . 13 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ ๐‘ก = โ„Ž)
4443oveq2d 7442 . . . . . . . . . . . 12 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ (๐‘“ ยทP ๐‘ก) = (๐‘“ ยทP โ„Ž))
4542, 44oveq12d 7444 . . . . . . . . . . 11 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ ((๐‘  ยทP ๐‘ข) +P (๐‘“ ยทP ๐‘ก)) = ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)))
4643oveq2d 7442 . . . . . . . . . . . 12 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ (๐‘  ยทP ๐‘ก) = (๐‘  ยทP โ„Ž))
4741oveq2d 7442 . . . . . . . . . . . 12 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ (๐‘“ ยทP ๐‘ข) = (๐‘“ ยทP ๐‘”))
4846, 47oveq12d 7444 . . . . . . . . . . 11 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ ((๐‘  ยทP ๐‘ก) +P (๐‘“ ยทP ๐‘ข)) = ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”)))
4945, 48opeq12d 4886 . . . . . . . . . 10 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ โŸจ((๐‘  ยทP ๐‘ข) +P (๐‘“ ยทP ๐‘ก)), ((๐‘  ยทP ๐‘ก) +P (๐‘“ ยทP ๐‘ข))โŸฉ = โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ)
5049eceq1d 8770 . . . . . . . . 9 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ [โŸจ((๐‘  ยทP ๐‘ข) +P (๐‘“ ยทP ๐‘ก)), ((๐‘  ยทP ๐‘ก) +P (๐‘“ ยทP ๐‘ข))โŸฉ] ~R = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R )
5150eqeq2d 2739 . . . . . . . 8 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ (๐‘ž = [โŸจ((๐‘  ยทP ๐‘ข) +P (๐‘“ ยทP ๐‘ก)), ((๐‘  ยทP ๐‘ก) +P (๐‘“ ยทP ๐‘ข))โŸฉ] ~R โ†” ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R ))
5240, 51anbi12d 630 . . . . . . 7 ((๐‘ข = ๐‘” โˆง ๐‘ก = โ„Ž) โ†’ (((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘ข) +P (๐‘“ ยทP ๐‘ก)), ((๐‘  ยทP ๐‘ก) +P (๐‘“ ยทP ๐‘ข))โŸฉ] ~R ) โ†” ((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R )))
5336, 52cbvex4vw 2037 . . . . . 6 (โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โ†” โˆƒ๐‘ โˆƒ๐‘“โˆƒ๐‘”โˆƒโ„Ž((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R ))
5453anbi2i 621 . . . . 5 ((โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R )) โ†” (โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง โˆƒ๐‘ โˆƒ๐‘“โˆƒ๐‘”โˆƒโ„Ž((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R )))
5554imbi1i 348 . . . 4 (((โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R )) โ†’ ๐‘ง = ๐‘ž) โ†” ((โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง โˆƒ๐‘ โˆƒ๐‘“โˆƒ๐‘”โˆƒโ„Ž((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R )) โ†’ ๐‘ง = ๐‘ž))
56552albii 1814 . . 3 (โˆ€๐‘งโˆ€๐‘ž((โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R )) โ†’ ๐‘ง = ๐‘ž) โ†” โˆ€๐‘งโˆ€๐‘ž((โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง โˆƒ๐‘ โˆƒ๐‘“โˆƒ๐‘”โˆƒโ„Ž((๐ด = [โŸจ๐‘ , ๐‘“โŸฉ] ~R โˆง ๐ต = [โŸจ๐‘”, โ„ŽโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘  ยทP ๐‘”) +P (๐‘“ ยทP โ„Ž)), ((๐‘  ยทP โ„Ž) +P (๐‘“ ยทP ๐‘”))โŸฉ] ~R )) โ†’ ๐‘ง = ๐‘ž))
5720, 56sylibr 233 . 2 ((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โ†’ โˆ€๐‘งโˆ€๐‘ž((โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R )) โ†’ ๐‘ง = ๐‘ž))
58 eqeq1 2732 . . . . 5 (๐‘ง = ๐‘ž โ†’ (๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R โ†” ๐‘ž = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ))
5958anbi2d 628 . . . 4 (๐‘ง = ๐‘ž โ†’ (((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โ†” ((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R )))
60594exbidv 1921 . . 3 (๐‘ง = ๐‘ž โ†’ (โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โ†” โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R )))
6160mo4 2555 . 2 (โˆƒ*๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โ†” โˆ€๐‘งโˆ€๐‘ž((โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ) โˆง โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ž = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R )) โ†’ ๐‘ง = ๐‘ž))
6257, 61sylibr 233 1 ((๐ด โˆˆ ((P ร— P) / ~R ) โˆง ๐ต โˆˆ ((P ร— P) / ~R )) โ†’ โˆƒ*๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐ด = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~R โˆง ๐ต = [โŸจ๐‘ข, ๐‘กโŸฉ] ~R ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทP ๐‘ข) +P (๐‘ฃ ยทP ๐‘ก)), ((๐‘ค ยทP ๐‘ก) +P (๐‘ฃ ยทP ๐‘ข))โŸฉ] ~R ))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 394  โˆ€wal 1531   = wceq 1533  โˆƒwex 1773   โˆˆ wcel 2098  โˆƒ*wmo 2527  โŸจcop 4638   class class class wbr 5152   ร— cxp 5680  (class class class)co 7426   Er wer 8728  [cec 8729   / cqs 8730  Pcnp 10890   +P cpp 10892   ยทP cmp 10893   ~R cer 10895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9672
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-oadd 8497  df-omul 8498  df-er 8731  df-ec 8733  df-qs 8737  df-ni 10903  df-pli 10904  df-mi 10905  df-lti 10906  df-plpq 10939  df-mpq 10940  df-ltpq 10941  df-enq 10942  df-nq 10943  df-erq 10944  df-plq 10945  df-mq 10946  df-1nq 10947  df-rq 10948  df-ltnq 10949  df-np 11012  df-plp 11014  df-mp 11015  df-ltp 11016  df-enr 11086
This theorem is referenced by:  mulsrpr  11107
  Copyright terms: Public domain W3C validator