ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addnnnq0 GIF version

Theorem addnnnq0 7450
Description: Addition of nonnegative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 22-Nov-2019.)
Assertion
Ref Expression
addnnnq0 (((๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ N) โˆง (๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N)) โ†’ ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 +Q0 [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 )

Proof of Theorem addnnnq0
Dummy variables ๐‘ฅ ๐‘ฆ ๐‘ง ๐‘ค ๐‘ฃ ๐‘ข ๐‘ก are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opelxpi 4660 . . . 4 ((๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ N) โ†’ โŸจ๐ด, ๐ตโŸฉ โˆˆ (ฯ‰ ร— N))
2 enq0ex 7440 . . . . 5 ~Q0 โˆˆ V
32ecelqsi 6591 . . . 4 (โŸจ๐ด, ๐ตโŸฉ โˆˆ (ฯ‰ ร— N) โ†’ [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ))
41, 3syl 14 . . 3 ((๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ N) โ†’ [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ))
5 opelxpi 4660 . . . 4 ((๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N) โ†’ โŸจ๐ถ, ๐ทโŸฉ โˆˆ (ฯ‰ ร— N))
62ecelqsi 6591 . . . 4 (โŸจ๐ถ, ๐ทโŸฉ โˆˆ (ฯ‰ ร— N) โ†’ [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ))
75, 6syl 14 . . 3 ((๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N) โ†’ [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ))
84, 7anim12i 338 . 2 (((๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ N) โˆง (๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N)) โ†’ ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ) โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 )))
9 eqid 2177 . . . 4 [โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0
10 eqid 2177 . . . 4 [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0
119, 10pm3.2i 272 . . 3 ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 )
12 eqid 2177 . . 3 [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0
13 opeq12 3782 . . . . . . . . 9 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ โŸจ๐‘ค, ๐‘ฃโŸฉ = โŸจ๐ด, ๐ตโŸฉ)
1413eceq1d 6573 . . . . . . . 8 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 )
1514eqeq2d 2189 . . . . . . 7 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โ†” [โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 ))
1615anbi1d 465 . . . . . 6 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โ†” ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 )))
17 simpl 109 . . . . . . . . . . 11 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ ๐‘ค = ๐ด)
1817oveq1d 5892 . . . . . . . . . 10 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ (๐‘ค ยทo ๐ท) = (๐ด ยทo ๐ท))
19 simpr 110 . . . . . . . . . . 11 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ ๐‘ฃ = ๐ต)
2019oveq1d 5892 . . . . . . . . . 10 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ (๐‘ฃ ยทo ๐ถ) = (๐ต ยทo ๐ถ))
2118, 20oveq12d 5895 . . . . . . . . 9 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)) = ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)))
2219oveq1d 5892 . . . . . . . . 9 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ (๐‘ฃ ยทo ๐ท) = (๐ต ยทo ๐ท))
2321, 22opeq12d 3788 . . . . . . . 8 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ โŸจ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)), (๐‘ฃ ยทo ๐ท)โŸฉ = โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ)
2423eceq1d 6573 . . . . . . 7 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ [โŸจ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 )
2524eqeq2d 2189 . . . . . 6 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ ([โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 โ†” [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ))
2616, 25anbi12d 473 . . . . 5 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ ((([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 ) โ†” (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 )))
2726spc2egv 2829 . . . 4 ((๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ N) โ†’ ((([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ โˆƒ๐‘คโˆƒ๐‘ฃ(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 )))
28 opeq12 3782 . . . . . . . . . 10 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ โŸจ๐‘ข, ๐‘กโŸฉ = โŸจ๐ถ, ๐ทโŸฉ)
2928eceq1d 6573 . . . . . . . . 9 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 )
3029eqeq2d 2189 . . . . . . . 8 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ ([โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 โ†” [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ))
3130anbi2d 464 . . . . . . 7 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โ†” ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 )))
32 simpr 110 . . . . . . . . . . . 12 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ ๐‘ก = ๐ท)
3332oveq2d 5893 . . . . . . . . . . 11 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ (๐‘ค ยทo ๐‘ก) = (๐‘ค ยทo ๐ท))
34 simpl 109 . . . . . . . . . . . 12 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ ๐‘ข = ๐ถ)
3534oveq2d 5893 . . . . . . . . . . 11 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ (๐‘ฃ ยทo ๐‘ข) = (๐‘ฃ ยทo ๐ถ))
3633, 35oveq12d 5895 . . . . . . . . . 10 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)) = ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)))
3732oveq2d 5893 . . . . . . . . . 10 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ (๐‘ฃ ยทo ๐‘ก) = (๐‘ฃ ยทo ๐ท))
3836, 37opeq12d 3788 . . . . . . . . 9 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ = โŸจ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)), (๐‘ฃ ยทo ๐ท)โŸฉ)
3938eceq1d 6573 . . . . . . . 8 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 )
4039eqeq2d 2189 . . . . . . 7 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ ([โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 โ†” [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 ))
4131, 40anbi12d 473 . . . . . 6 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ ((([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ) โ†” (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 )))
4241spc2egv 2829 . . . . 5 ((๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N) โ†’ ((([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ โˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 )))
43422eximdv 1882 . . . 4 ((๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N) โ†’ (โˆƒ๐‘คโˆƒ๐‘ฃ(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐ท) +o (๐‘ฃ ยทo ๐ถ)), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 )))
4427, 43sylan9 409 . . 3 (((๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ N) โˆง (๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N)) โ†’ ((([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 )))
4511, 12, 44mp2ani 432 . 2 (((๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ N) โˆง (๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N)) โ†’ โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ))
46 ecexg 6541 . . . 4 ( ~Q0 โˆˆ V โ†’ [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 โˆˆ V)
472, 46ax-mp 5 . . 3 [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 โˆˆ V
48 simp1 997 . . . . . . . 8 ((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆง ๐‘ง = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ ๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 )
4948eqeq1d 2186 . . . . . . 7 ((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆง ๐‘ง = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ (๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โ†” [โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 ))
50 simp2 998 . . . . . . . 8 ((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆง ๐‘ง = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 )
5150eqeq1d 2186 . . . . . . 7 ((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆง ๐‘ง = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ (๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 โ†” [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ))
5249, 51anbi12d 473 . . . . . 6 ((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆง ๐‘ง = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ ((๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โ†” ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 )))
53 simp3 999 . . . . . . 7 ((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆง ๐‘ง = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ ๐‘ง = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 )
5453eqeq1d 2186 . . . . . 6 ((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆง ๐‘ง = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ (๐‘ง = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 โ†” [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ))
5552, 54anbi12d 473 . . . . 5 ((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆง ๐‘ง = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ (((๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ) โ†” (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 )))
56554exbidv 1870 . . . 4 ((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆง ๐‘ง = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ (โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ) โ†” โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 )))
57 addnq0mo 7448 . . . 4 ((๐‘ฅ โˆˆ ((ฯ‰ ร— N) / ~Q0 ) โˆง ๐‘ฆ โˆˆ ((ฯ‰ ร— N) / ~Q0 )) โ†’ โˆƒ*๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ))
58 dfplq0qs 7431 . . . 4 +Q0 = {โŸจโŸจ๐‘ฅ, ๐‘ฆโŸฉ, ๐‘งโŸฉ โˆฃ ((๐‘ฅ โˆˆ ((ฯ‰ ร— N) / ~Q0 ) โˆง ๐‘ฆ โˆˆ ((ฯ‰ ร— N) / ~Q0 )) โˆง โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง ๐‘ง = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ))}
5956, 57, 58ovig 5998 . . 3 (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ) โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 โˆˆ V) โ†’ (โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ) โ†’ ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 +Q0 [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ))
6047, 59mp3an3 1326 . 2 (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ) โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 )) โ†’ (โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ((๐‘ค ยทo ๐‘ก) +o (๐‘ฃ ยทo ๐‘ข)), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ) โ†’ ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 +Q0 [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ))
618, 45, 60sylc 62 1 (((๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ N) โˆง (๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N)) โ†’ ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 +Q0 [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) = [โŸจ((๐ด ยทo ๐ท) +o (๐ต ยทo ๐ถ)), (๐ต ยทo ๐ท)โŸฉ] ~Q0 )
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โˆง w3a 978   = wceq 1353  โˆƒwex 1492   โˆˆ wcel 2148  Vcvv 2739  โŸจcop 3597  ฯ‰com 4591   ร— cxp 4626  (class class class)co 5877   +o coa 6416   ยทo comu 6417  [cec 6535   / cqs 6536  Ncnpi 7273   ~Q0 ceq0 7287   +Q0 cplq0 7290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-ov 5880  df-oprab 5881  df-mpo 5882  df-1st 6143  df-2nd 6144  df-recs 6308  df-irdg 6373  df-oadd 6423  df-omul 6424  df-er 6537  df-ec 6539  df-qs 6543  df-ni 7305  df-mi 7307  df-enq0 7425  df-nq0 7426  df-plq0 7428
This theorem is referenced by:  addclnq0  7452  nqpnq0nq  7454  nqnq0a  7455  nq0a0  7458  nnanq0  7459  distrnq0  7460  addassnq0  7463
  Copyright terms: Public domain W3C validator