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

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

Proof of Theorem mulnnnq0
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 ๐ท)โŸฉ] ~Q0 = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0
13 opeq12 3782 . . . . . 6 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ โŸจ๐‘ค, ๐‘ฃโŸฉ = โŸจ๐ด, ๐ตโŸฉ)
14 eceq1 6572 . . . . . . . . 9 (โŸจ๐‘ค, ๐‘ฃโŸฉ = โŸจ๐ด, ๐ตโŸฉ โ†’ [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 )
1514eqeq2d 2189 . . . . . . . 8 (โŸจ๐‘ค, ๐‘ฃโŸฉ = โŸจ๐ด, ๐ตโŸฉ โ†’ ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โ†” [โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 ))
1615anbi1d 465 . . . . . . 7 (โŸจ๐‘ค, ๐‘ฃโŸฉ = โŸจ๐ด, ๐ตโŸฉ โ†’ (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โ†” ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 )))
17 vex 2742 . . . . . . . . . . 11 ๐‘ค โˆˆ V
18 vex 2742 . . . . . . . . . . 11 ๐‘ฃ โˆˆ V
1917, 18opth 4239 . . . . . . . . . 10 (โŸจ๐‘ค, ๐‘ฃโŸฉ = โŸจ๐ด, ๐ตโŸฉ โ†” (๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต))
20 oveq1 5884 . . . . . . . . . . . 12 (๐‘ค = ๐ด โ†’ (๐‘ค ยทo ๐ถ) = (๐ด ยทo ๐ถ))
2120adantr 276 . . . . . . . . . . 11 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ (๐‘ค ยทo ๐ถ) = (๐ด ยทo ๐ถ))
22 oveq1 5884 . . . . . . . . . . . 12 (๐‘ฃ = ๐ต โ†’ (๐‘ฃ ยทo ๐ท) = (๐ต ยทo ๐ท))
2322adantl 277 . . . . . . . . . . 11 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ (๐‘ฃ ยทo ๐ท) = (๐ต ยทo ๐ท))
2421, 23opeq12d 3788 . . . . . . . . . 10 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ = โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ)
2519, 24sylbi 121 . . . . . . . . 9 (โŸจ๐‘ค, ๐‘ฃโŸฉ = โŸจ๐ด, ๐ตโŸฉ โ†’ โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ = โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ)
2625eceq1d 6573 . . . . . . . 8 (โŸจ๐‘ค, ๐‘ฃโŸฉ = โŸจ๐ด, ๐ตโŸฉ โ†’ [โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 )
2726eqeq2d 2189 . . . . . . 7 (โŸจ๐‘ค, ๐‘ฃโŸฉ = โŸจ๐ด, ๐ตโŸฉ โ†’ ([โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 โ†” [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ))
2816, 27anbi12d 473 . . . . . 6 (โŸจ๐‘ค, ๐‘ฃโŸฉ = โŸจ๐ด, ๐ตโŸฉ โ†’ ((([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 ) โ†” (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 )))
2913, 28syl 14 . . . . 5 ((๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต) โ†’ ((([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 ) โ†” (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 )))
3029spc2egv 2829 . . . 4 ((๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ N) โ†’ ((([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ โˆƒ๐‘คโˆƒ๐‘ฃ(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 )))
31 opeq12 3782 . . . . . . 7 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ โŸจ๐‘ข, ๐‘กโŸฉ = โŸจ๐ถ, ๐ทโŸฉ)
32 eceq1 6572 . . . . . . . . . 10 (โŸจ๐‘ข, ๐‘กโŸฉ = โŸจ๐ถ, ๐ทโŸฉ โ†’ [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 )
3332eqeq2d 2189 . . . . . . . . 9 (โŸจ๐‘ข, ๐‘กโŸฉ = โŸจ๐ถ, ๐ทโŸฉ โ†’ ([โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 โ†” [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ))
3433anbi2d 464 . . . . . . . 8 (โŸจ๐‘ข, ๐‘กโŸฉ = โŸจ๐ถ, ๐ทโŸฉ โ†’ (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โ†” ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 )))
35 vex 2742 . . . . . . . . . . . 12 ๐‘ข โˆˆ V
36 vex 2742 . . . . . . . . . . . 12 ๐‘ก โˆˆ V
3735, 36opth 4239 . . . . . . . . . . 11 (โŸจ๐‘ข, ๐‘กโŸฉ = โŸจ๐ถ, ๐ทโŸฉ โ†” (๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท))
38 oveq2 5885 . . . . . . . . . . . . 13 (๐‘ข = ๐ถ โ†’ (๐‘ค ยทo ๐‘ข) = (๐‘ค ยทo ๐ถ))
3938adantr 276 . . . . . . . . . . . 12 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ (๐‘ค ยทo ๐‘ข) = (๐‘ค ยทo ๐ถ))
40 oveq2 5885 . . . . . . . . . . . . 13 (๐‘ก = ๐ท โ†’ (๐‘ฃ ยทo ๐‘ก) = (๐‘ฃ ยทo ๐ท))
4140adantl 277 . . . . . . . . . . . 12 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ (๐‘ฃ ยทo ๐‘ก) = (๐‘ฃ ยทo ๐ท))
4239, 41opeq12d 3788 . . . . . . . . . . 11 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ = โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ)
4337, 42sylbi 121 . . . . . . . . . 10 (โŸจ๐‘ข, ๐‘กโŸฉ = โŸจ๐ถ, ๐ทโŸฉ โ†’ โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ = โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ)
4443eceq1d 6573 . . . . . . . . 9 (โŸจ๐‘ข, ๐‘กโŸฉ = โŸจ๐ถ, ๐ทโŸฉ โ†’ [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 )
4544eqeq2d 2189 . . . . . . . 8 (โŸจ๐‘ข, ๐‘กโŸฉ = โŸจ๐ถ, ๐ทโŸฉ โ†’ ([โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 โ†” [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 ))
4634, 45anbi12d 473 . . . . . . 7 (โŸจ๐‘ข, ๐‘กโŸฉ = โŸจ๐ถ, ๐ทโŸฉ โ†’ ((([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ) โ†” (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 )))
4731, 46syl 14 . . . . . 6 ((๐‘ข = ๐ถ โˆง ๐‘ก = ๐ท) โ†’ ((([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ) โ†” (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 )))
4847spc2egv 2829 . . . . 5 ((๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N) โ†’ ((([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ โˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 )))
49482eximdv 1882 . . . 4 ((๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N) โ†’ (โˆƒ๐‘คโˆƒ๐‘ฃ(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐ถ), (๐‘ฃ ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 )))
5030, 49sylan9 409 . . 3 (((๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ N) โˆง (๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N)) โ†’ ((([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 )))
5111, 12, 50mp2ani 432 . 2 (((๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ N) โˆง (๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N)) โ†’ โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ))
52 ecexg 6541 . . . 4 ( ~Q0 โˆˆ V โ†’ [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 โˆˆ V)
532, 52ax-mp 5 . . 3 [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 โˆˆ V
54 eqeq1 2184 . . . . . . . 8 (๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โ†’ (๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โ†” [โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 ))
55 eqeq1 2184 . . . . . . . 8 (๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โ†’ (๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 โ†” [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ))
5654, 55bi2anan9 606 . . . . . . 7 ((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โ†’ ((๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โ†” ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 )))
57 eqeq1 2184 . . . . . . 7 (๐‘ง = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 โ†’ (๐‘ง = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 โ†” [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ))
5856, 57bi2anan9 606 . . . . . 6 (((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) โˆง ๐‘ง = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ (((๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง ๐‘ง = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ) โ†” (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 )))
59583impa 1194 . . . . 5 ((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆง ๐‘ง = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ (((๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง ๐‘ง = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ) โ†” (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 )))
60594exbidv 1870 . . . 4 ((๐‘ฅ = [โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆง ๐‘ง = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ) โ†’ (โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง ๐‘ง = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ) โ†” โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 )))
61 mulnq0mo 7449 . . . 4 ((๐‘ฅ โˆˆ ((ฯ‰ ร— N) / ~Q0 ) โˆง ๐‘ฆ โˆˆ ((ฯ‰ ร— N) / ~Q0 )) โ†’ โˆƒ*๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง ๐‘ง = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ))
62 dfmq0qs 7430 . . . 4 ยทQ0 = {โŸจโŸจ๐‘ฅ, ๐‘ฆโŸฉ, ๐‘งโŸฉ โˆฃ ((๐‘ฅ โˆˆ ((ฯ‰ ร— N) / ~Q0 ) โˆง ๐‘ฆ โˆˆ ((ฯ‰ ร— N) / ~Q0 )) โˆง โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก((๐‘ฅ = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง ๐‘ฆ = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง ๐‘ง = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ))}
6360, 61, 62ovig 5998 . . 3 (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ) โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 โˆˆ V) โ†’ (โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ) โ†’ ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 ยทQ0 [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ))
6453, 63mp3an3 1326 . 2 (([โŸจ๐ด, ๐ตโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ) โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 )) โ†’ (โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ขโˆƒ๐‘ก(([โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐‘ค, ๐‘ฃโŸฉ] ~Q0 โˆง [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 = [โŸจ๐‘ข, ๐‘กโŸฉ] ~Q0 ) โˆง [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 = [โŸจ(๐‘ค ยทo ๐‘ข), (๐‘ฃ ยทo ๐‘ก)โŸฉ] ~Q0 ) โ†’ ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 ยทQ0 [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 ))
658, 51, 64sylc 62 1 (((๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ N) โˆง (๐ถ โˆˆ ฯ‰ โˆง ๐ท โˆˆ N)) โ†’ ([โŸจ๐ด, ๐ตโŸฉ] ~Q0 ยทQ0 [โŸจ๐ถ, ๐ทโŸฉ] ~Q0 ) = [โŸจ(๐ด ยทo ๐ถ), (๐ต ยทo ๐ท)โŸฉ] ~Q0 )
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 978   = wceq 1353  โˆƒwex 1492   โˆˆ wcel 2148  Vcvv 2739  โŸจcop 3597  ฯ‰com 4591   ร— cxp 4626  (class class class)co 5877   ยทo comu 6417  [cec 6535   / cqs 6536  Ncnpi 7273   ~Q0 ceq0 7287   ยทQ0 cmq0 7291
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-mq0 7429
This theorem is referenced by:  mulclnq0  7453  nqnq0m  7456  nq0m0r  7457  distrnq0  7460  mulcomnq0  7461  nq02m  7466
  Copyright terms: Public domain W3C validator