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

 Description: Addition of nonnegative fractions is associative. (Contributed by Jim Kingdon, 29-Nov-2019.)
Assertion
Ref Expression
addassnq0 ((𝐴Q0𝐵Q0𝐶Q0) → ((𝐴 +Q0 𝐵) +Q0 𝐶) = (𝐴 +Q0 (𝐵 +Q0 𝐶)))

Proof of Theorem addassnq0
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nq0 7328 . . . 4 Q0 = ((ω × N) / ~Q0 )
2 oveq2 5826 . . . . . . 7 ([⟨𝑧, 𝑤⟩] ~Q0 = 𝐵 → (𝐴 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) = (𝐴 +Q0 𝐵))
32oveq1d 5833 . . . . . 6 ([⟨𝑧, 𝑤⟩] ~Q0 = 𝐵 → ((𝐴 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = ((𝐴 +Q0 𝐵) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))
4 oveq1 5825 . . . . . . 7 ([⟨𝑧, 𝑤⟩] ~Q0 = 𝐵 → ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = (𝐵 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))
54oveq2d 5834 . . . . . 6 ([⟨𝑧, 𝑤⟩] ~Q0 = 𝐵 → (𝐴 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )) = (𝐴 +Q0 (𝐵 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )))
63, 5eqeq12d 2172 . . . . 5 ([⟨𝑧, 𝑤⟩] ~Q0 = 𝐵 → (((𝐴 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = (𝐴 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )) ↔ ((𝐴 +Q0 𝐵) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = (𝐴 +Q0 (𝐵 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))))
76imbi2d 229 . . . 4 ([⟨𝑧, 𝑤⟩] ~Q0 = 𝐵 → ((𝐴Q0 → ((𝐴 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = (𝐴 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))) ↔ (𝐴Q0 → ((𝐴 +Q0 𝐵) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = (𝐴 +Q0 (𝐵 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )))))
8 oveq2 5826 . . . . . 6 ([⟨𝑣, 𝑢⟩] ~Q0 = 𝐶 → ((𝐴 +Q0 𝐵) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = ((𝐴 +Q0 𝐵) +Q0 𝐶))
9 oveq2 5826 . . . . . . 7 ([⟨𝑣, 𝑢⟩] ~Q0 = 𝐶 → (𝐵 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = (𝐵 +Q0 𝐶))
109oveq2d 5834 . . . . . 6 ([⟨𝑣, 𝑢⟩] ~Q0 = 𝐶 → (𝐴 +Q0 (𝐵 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )) = (𝐴 +Q0 (𝐵 +Q0 𝐶)))
118, 10eqeq12d 2172 . . . . 5 ([⟨𝑣, 𝑢⟩] ~Q0 = 𝐶 → (((𝐴 +Q0 𝐵) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = (𝐴 +Q0 (𝐵 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )) ↔ ((𝐴 +Q0 𝐵) +Q0 𝐶) = (𝐴 +Q0 (𝐵 +Q0 𝐶))))
1211imbi2d 229 . . . 4 ([⟨𝑣, 𝑢⟩] ~Q0 = 𝐶 → ((𝐴Q0 → ((𝐴 +Q0 𝐵) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = (𝐴 +Q0 (𝐵 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))) ↔ (𝐴Q0 → ((𝐴 +Q0 𝐵) +Q0 𝐶) = (𝐴 +Q0 (𝐵 +Q0 𝐶)))))
13 oveq1 5825 . . . . . . . . 9 ([⟨𝑥, 𝑦⟩] ~Q0 = 𝐴 → ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) = (𝐴 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ))
1413oveq1d 5833 . . . . . . . 8 ([⟨𝑥, 𝑦⟩] ~Q0 = 𝐴 → (([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = ((𝐴 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))
15 oveq1 5825 . . . . . . . 8 ([⟨𝑥, 𝑦⟩] ~Q0 = 𝐴 → ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )) = (𝐴 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )))
1614, 15eqeq12d 2172 . . . . . . 7 ([⟨𝑥, 𝑦⟩] ~Q0 = 𝐴 → ((([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )) ↔ ((𝐴 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = (𝐴 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))))
1716imbi2d 229 . . . . . 6 ([⟨𝑥, 𝑦⟩] ~Q0 = 𝐴 → ((((𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))) ↔ (((𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → ((𝐴 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = (𝐴 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )))))
18 simp1l 1006 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → 𝑥 ∈ ω)
19 simp2r 1009 . . . . . . . . . . . . . 14 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → 𝑤N)
20 pinn 7212 . . . . . . . . . . . . . 14 (𝑤N𝑤 ∈ ω)
2119, 20syl 14 . . . . . . . . . . . . 13 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → 𝑤 ∈ ω)
22 simp3r 1011 . . . . . . . . . . . . . 14 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → 𝑢N)
23 pinn 7212 . . . . . . . . . . . . . 14 (𝑢N𝑢 ∈ ω)
2422, 23syl 14 . . . . . . . . . . . . 13 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → 𝑢 ∈ ω)
25 nnmcl 6421 . . . . . . . . . . . . 13 ((𝑤 ∈ ω ∧ 𝑢 ∈ ω) → (𝑤 ·o 𝑢) ∈ ω)
2621, 24, 25syl2anc 409 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (𝑤 ·o 𝑢) ∈ ω)
27 nnmcl 6421 . . . . . . . . . . . 12 ((𝑥 ∈ ω ∧ (𝑤 ·o 𝑢) ∈ ω) → (𝑥 ·o (𝑤 ·o 𝑢)) ∈ ω)
2818, 26, 27syl2anc 409 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (𝑥 ·o (𝑤 ·o 𝑢)) ∈ ω)
29 simp1r 1007 . . . . . . . . . . . . 13 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → 𝑦N)
30 pinn 7212 . . . . . . . . . . . . 13 (𝑦N𝑦 ∈ ω)
3129, 30syl 14 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → 𝑦 ∈ ω)
32 simp2l 1008 . . . . . . . . . . . . 13 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → 𝑧 ∈ ω)
33 nnmcl 6421 . . . . . . . . . . . . 13 ((𝑧 ∈ ω ∧ 𝑢 ∈ ω) → (𝑧 ·o 𝑢) ∈ ω)
3432, 24, 33syl2anc 409 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (𝑧 ·o 𝑢) ∈ ω)
35 nnmcl 6421 . . . . . . . . . . . 12 ((𝑦 ∈ ω ∧ (𝑧 ·o 𝑢) ∈ ω) → (𝑦 ·o (𝑧 ·o 𝑢)) ∈ ω)
3631, 34, 35syl2anc 409 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (𝑦 ·o (𝑧 ·o 𝑢)) ∈ ω)
37 simp3l 1010 . . . . . . . . . . . . 13 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → 𝑣 ∈ ω)
38 nnmcl 6421 . . . . . . . . . . . . 13 ((𝑤 ∈ ω ∧ 𝑣 ∈ ω) → (𝑤 ·o 𝑣) ∈ ω)
3921, 37, 38syl2anc 409 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (𝑤 ·o 𝑣) ∈ ω)
40 nnmcl 6421 . . . . . . . . . . . 12 ((𝑦 ∈ ω ∧ (𝑤 ·o 𝑣) ∈ ω) → (𝑦 ·o (𝑤 ·o 𝑣)) ∈ ω)
4131, 39, 40syl2anc 409 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (𝑦 ·o (𝑤 ·o 𝑣)) ∈ ω)
42 nnaass 6425 . . . . . . . . . . 11 (((𝑥 ·o (𝑤 ·o 𝑢)) ∈ ω ∧ (𝑦 ·o (𝑧 ·o 𝑢)) ∈ ω ∧ (𝑦 ·o (𝑤 ·o 𝑣)) ∈ ω) → (((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o (𝑧 ·o 𝑢))) +o (𝑦 ·o (𝑤 ·o 𝑣))) = ((𝑥 ·o (𝑤 ·o 𝑢)) +o ((𝑦 ·o (𝑧 ·o 𝑢)) +o (𝑦 ·o (𝑤 ·o 𝑣)))))
4328, 36, 41, 42syl3anc 1220 . . . . . . . . . 10 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o (𝑧 ·o 𝑢))) +o (𝑦 ·o (𝑤 ·o 𝑣))) = ((𝑥 ·o (𝑤 ·o 𝑢)) +o ((𝑦 ·o (𝑧 ·o 𝑢)) +o (𝑦 ·o (𝑤 ·o 𝑣)))))
44 nnmcom 6429 . . . . . . . . . . . . 13 ((𝑓 ∈ ω ∧ 𝑔 ∈ ω) → (𝑓 ·o 𝑔) = (𝑔 ·o 𝑓))
4544adantl 275 . . . . . . . . . . . 12 ((((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑓 ·o 𝑔) = (𝑔 ·o 𝑓))
46 nndir 6430 . . . . . . . . . . . . 13 ((𝑓 ∈ ω ∧ 𝑔 ∈ ω ∧ ∈ ω) → ((𝑓 +o 𝑔) ·o ) = ((𝑓 ·o ) +o (𝑔 ·o )))
4746adantl 275 . . . . . . . . . . . 12 ((((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω ∧ ∈ ω)) → ((𝑓 +o 𝑔) ·o ) = ((𝑓 ·o ) +o (𝑔 ·o )))
48 nnmass 6427 . . . . . . . . . . . . 13 ((𝑓 ∈ ω ∧ 𝑔 ∈ ω ∧ ∈ ω) → ((𝑓 ·o 𝑔) ·o ) = (𝑓 ·o (𝑔 ·o )))
4948adantl 275 . . . . . . . . . . . 12 ((((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω ∧ ∈ ω)) → ((𝑓 ·o 𝑔) ·o ) = (𝑓 ·o (𝑔 ·o )))
50 nnmcl 6421 . . . . . . . . . . . . 13 ((𝑓 ∈ ω ∧ 𝑔 ∈ ω) → (𝑓 ·o 𝑔) ∈ ω)
5150adantl 275 . . . . . . . . . . . 12 ((((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑓 ·o 𝑔) ∈ ω)
5245, 47, 49, 51, 18, 31, 21, 32, 24caovdilemd 6006 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ·o 𝑢) = ((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o (𝑧 ·o 𝑢))))
53 nnmass 6427 . . . . . . . . . . . 12 ((𝑦 ∈ ω ∧ 𝑤 ∈ ω ∧ 𝑣 ∈ ω) → ((𝑦 ·o 𝑤) ·o 𝑣) = (𝑦 ·o (𝑤 ·o 𝑣)))
5431, 21, 37, 53syl3anc 1220 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → ((𝑦 ·o 𝑤) ·o 𝑣) = (𝑦 ·o (𝑤 ·o 𝑣)))
5552, 54oveq12d 5836 . . . . . . . . . 10 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → ((((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ·o 𝑢) +o ((𝑦 ·o 𝑤) ·o 𝑣)) = (((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o (𝑧 ·o 𝑢))) +o (𝑦 ·o (𝑤 ·o 𝑣))))
56 nndi 6426 . . . . . . . . . . . 12 ((𝑦 ∈ ω ∧ (𝑧 ·o 𝑢) ∈ ω ∧ (𝑤 ·o 𝑣) ∈ ω) → (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣))) = ((𝑦 ·o (𝑧 ·o 𝑢)) +o (𝑦 ·o (𝑤 ·o 𝑣))))
5731, 34, 39, 56syl3anc 1220 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣))) = ((𝑦 ·o (𝑧 ·o 𝑢)) +o (𝑦 ·o (𝑤 ·o 𝑣))))
5857oveq2d 5834 . . . . . . . . . 10 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → ((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)))) = ((𝑥 ·o (𝑤 ·o 𝑢)) +o ((𝑦 ·o (𝑧 ·o 𝑢)) +o (𝑦 ·o (𝑤 ·o 𝑣)))))
5943, 55, 583eqtr4d 2200 . . . . . . . . 9 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → ((((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ·o 𝑢) +o ((𝑦 ·o 𝑤) ·o 𝑣)) = ((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)))))
60 nnmass 6427 . . . . . . . . . 10 ((𝑦 ∈ ω ∧ 𝑤 ∈ ω ∧ 𝑢 ∈ ω) → ((𝑦 ·o 𝑤) ·o 𝑢) = (𝑦 ·o (𝑤 ·o 𝑢)))
6131, 21, 24, 60syl3anc 1220 . . . . . . . . 9 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → ((𝑦 ·o 𝑤) ·o 𝑢) = (𝑦 ·o (𝑤 ·o 𝑢)))
62 opeq12 3743 . . . . . . . . . 10 ((((((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ·o 𝑢) +o ((𝑦 ·o 𝑤) ·o 𝑣)) = ((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)))) ∧ ((𝑦 ·o 𝑤) ·o 𝑢) = (𝑦 ·o (𝑤 ·o 𝑢))) → ⟨((((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ·o 𝑢) +o ((𝑦 ·o 𝑤) ·o 𝑣)), ((𝑦 ·o 𝑤) ·o 𝑢)⟩ = ⟨((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)))), (𝑦 ·o (𝑤 ·o 𝑢))⟩)
6362eceq1d 6509 . . . . . . . . 9 ((((((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ·o 𝑢) +o ((𝑦 ·o 𝑤) ·o 𝑣)) = ((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)))) ∧ ((𝑦 ·o 𝑤) ·o 𝑢) = (𝑦 ·o (𝑤 ·o 𝑢))) → [⟨((((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ·o 𝑢) +o ((𝑦 ·o 𝑤) ·o 𝑣)), ((𝑦 ·o 𝑤) ·o 𝑢)⟩] ~Q0 = [⟨((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)))), (𝑦 ·o (𝑤 ·o 𝑢))⟩] ~Q0 )
6459, 61, 63syl2anc 409 . . . . . . . 8 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → [⟨((((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ·o 𝑢) +o ((𝑦 ·o 𝑤) ·o 𝑣)), ((𝑦 ·o 𝑤) ·o 𝑢)⟩] ~Q0 = [⟨((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)))), (𝑦 ·o (𝑤 ·o 𝑢))⟩] ~Q0 )
65 addnnnq0 7352 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N)) → ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) = [⟨((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)), (𝑦 ·o 𝑤)⟩] ~Q0 )
6665oveq1d 5833 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N)) → (([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = ([⟨((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)), (𝑦 ·o 𝑤)⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))
6766adantr 274 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N)) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = ([⟨((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)), (𝑦 ·o 𝑤)⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))
68 addassnq0lemcl 7364 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N)) → (((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ∈ ω ∧ (𝑦 ·o 𝑤) ∈ N))
69 addnnnq0 7352 . . . . . . . . . . 11 (((((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ∈ ω ∧ (𝑦 ·o 𝑤) ∈ N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → ([⟨((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)), (𝑦 ·o 𝑤)⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = [⟨((((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ·o 𝑢) +o ((𝑦 ·o 𝑤) ·o 𝑣)), ((𝑦 ·o 𝑤) ·o 𝑢)⟩] ~Q0 )
7068, 69sylan 281 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N)) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → ([⟨((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)), (𝑦 ·o 𝑤)⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = [⟨((((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ·o 𝑢) +o ((𝑦 ·o 𝑤) ·o 𝑣)), ((𝑦 ·o 𝑤) ·o 𝑢)⟩] ~Q0 )
7167, 70eqtrd 2190 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N)) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = [⟨((((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ·o 𝑢) +o ((𝑦 ·o 𝑤) ·o 𝑣)), ((𝑦 ·o 𝑤) ·o 𝑢)⟩] ~Q0 )
72713impa 1177 . . . . . . . 8 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = [⟨((((𝑥 ·o 𝑤) +o (𝑦 ·o 𝑧)) ·o 𝑢) +o ((𝑦 ·o 𝑤) ·o 𝑣)), ((𝑦 ·o 𝑤) ·o 𝑢)⟩] ~Q0 )
73 addnnnq0 7352 . . . . . . . . . . . 12 (((𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = [⟨((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)), (𝑤 ·o 𝑢)⟩] ~Q0 )
7473oveq2d 5834 . . . . . . . . . . 11 (((𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )) = ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)), (𝑤 ·o 𝑢)⟩] ~Q0 ))
7574adantl 275 . . . . . . . . . 10 (((𝑥 ∈ ω ∧ 𝑦N) ∧ ((𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N))) → ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )) = ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)), (𝑤 ·o 𝑢)⟩] ~Q0 ))
76 addassnq0lemcl 7364 . . . . . . . . . . 11 (((𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)) ∈ ω ∧ (𝑤 ·o 𝑢) ∈ N))
77 addnnnq0 7352 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)) ∈ ω ∧ (𝑤 ·o 𝑢) ∈ N)) → ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)), (𝑤 ·o 𝑢)⟩] ~Q0 ) = [⟨((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)))), (𝑦 ·o (𝑤 ·o 𝑢))⟩] ~Q0 )
7876, 77sylan2 284 . . . . . . . . . 10 (((𝑥 ∈ ω ∧ 𝑦N) ∧ ((𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N))) → ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)), (𝑤 ·o 𝑢)⟩] ~Q0 ) = [⟨((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)))), (𝑦 ·o (𝑤 ·o 𝑢))⟩] ~Q0 )
7975, 78eqtrd 2190 . . . . . . . . 9 (((𝑥 ∈ ω ∧ 𝑦N) ∧ ((𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N))) → ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )) = [⟨((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)))), (𝑦 ·o (𝑤 ·o 𝑢))⟩] ~Q0 )
80793impb 1181 . . . . . . . 8 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )) = [⟨((𝑥 ·o (𝑤 ·o 𝑢)) +o (𝑦 ·o ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)))), (𝑦 ·o (𝑤 ·o 𝑢))⟩] ~Q0 )
8164, 72, 803eqtr4d 2200 . . . . . . 7 (((𝑥 ∈ ω ∧ 𝑦N) ∧ (𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 )))
82813expib 1188 . . . . . 6 ((𝑥 ∈ ω ∧ 𝑦N) → (((𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (([⟨𝑥, 𝑦⟩] ~Q0 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = ([⟨𝑥, 𝑦⟩] ~Q0 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))))
831, 17, 82ecoptocl 6560 . . . . 5 (𝐴Q0 → (((𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → ((𝐴 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = (𝐴 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))))
8483com12 30 . . . 4 (((𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑣 ∈ ω ∧ 𝑢N)) → (𝐴Q0 → ((𝐴 +Q0 [⟨𝑧, 𝑤⟩] ~Q0 ) +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ) = (𝐴 +Q0 ([⟨𝑧, 𝑤⟩] ~Q0 +Q0 [⟨𝑣, 𝑢⟩] ~Q0 ))))
851, 7, 12, 842ecoptocl 6561 . . 3 ((𝐵Q0𝐶Q0) → (𝐴Q0 → ((𝐴 +Q0 𝐵) +Q0 𝐶) = (𝐴 +Q0 (𝐵 +Q0 𝐶))))
8685com12 30 . 2 (𝐴Q0 → ((𝐵Q0𝐶Q0) → ((𝐴 +Q0 𝐵) +Q0 𝐶) = (𝐴 +Q0 (𝐵 +Q0 𝐶))))
87863impib 1183 1 ((𝐴Q0𝐵Q0𝐶Q0) → ((𝐴 +Q0 𝐵) +Q0 𝐶) = (𝐴 +Q0 (𝐵 +Q0 𝐶)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963   = wceq 1335   ∈ wcel 2128  ⟨cop 3563  ωcom 4547  (class class class)co 5818   +o coa 6354   ·o comu 6355  [cec 6471  Ncnpi 7175   ~Q0 ceq0 7189  Q0cnq0 7190   +Q0 cplq0 7192 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-iinf 4545 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4252  df-iord 4325  df-on 4327  df-suc 4330  df-iom 4548  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-f1 5172  df-fo 5173  df-f1o 5174  df-fv 5175  df-ov 5821  df-oprab 5822  df-mpo 5823  df-1st 6082  df-2nd 6083  df-recs 6246  df-irdg 6311  df-oadd 6361  df-omul 6362  df-er 6473  df-ec 6475  df-qs 6479  df-ni 7207  df-mi 7209  df-enq0 7327  df-nq0 7328  df-plq0 7330 This theorem is referenced by:  prarloclemcalc  7405
 Copyright terms: Public domain W3C validator