Theorem comcom 435

Description: Commutation is symmetric. Kalmbach 83 p. 22.

Hypothesis

Ref	Expression
comcom.1	a C b

Assertion

Ref	Expression
comcom	b C a

Proof of Theorem comcom

Step	Hyp	Ref	Expression
1		ax-a2 30	. . . . . . . . . 10 (a_|_ v b) = (b v a_|_)
2	1	ran 71	. . . . . . . . 9 ((a_|_ v b) ^ b) = ((b v a_|_) ^ b)
3		ancom 68	. . . . . . . . 9 ((b v a_|_) ^ b) = (b ^ (b v a_|_))
4	2, 3	ax-r2 35	. . . . . . . 8 ((a_|_ v b) ^ b) = (b ^ (b v a_|_))
5		a5c 113	. . . . . . . 8 (b ^ (b v a_|_)) = b
6	4, 5	ax-r2 35	. . . . . . 7 ((a_|_ v b) ^ b) = b
7	6	lan 70	. . . . . 6 ((a_|_ v b_|_) ^ ((a_|_ v b) ^ b)) = ((a_|_ v b_|_) ^ b)
8		comcom.1	. . . . . . . . . . . 12 a C b
9	8	df-c2 125	. . . . . . . . . . 11 a = ((a ^ b) v (a ^ b_|_))
10		df-a 39	. . . . . . . . . . . 12 (a ^ b) = (a_|_ v b_|_)_|_
11		anor1 80	. . . . . . . . . . . 12 (a ^ b_|_) = (a_|_ v b)_|_
12	10, 11	2or 67	. . . . . . . . . . 11 ((a ^ b) v (a ^ b_|_)) = ((a_|_ v b_|_)_|_ v (a_|_ v b)_|_)
13	9, 12	ax-r2 35	. . . . . . . . . 10 a = ((a_|_ v b_|_)_|_ v (a_|_ v b)_|_)
14	13	ax-r4 36	. . . . . . . . 9 a_|_ = ((a_|_ v b_|_)_|_ v (a_|_ v b)_|_)_|_
15		df-a 39	. . . . . . . . . 10 ((a_|_ v b_|_) ^ (a_|_ v b)) = ((a_|_ v b_|_)_|_ v (a_|_ v b)_|_)_|_
16	15	ax-r1 34	. . . . . . . . 9 ((a_|_ v b_|_)_|_ v (a_|_ v b)_|_)_|_ = ((a_|_ v b_|_) ^ (a_|_ v b))
17	14, 16	ax-r2 35	. . . . . . . 8 a_|_ = ((a_|_ v b_|_) ^ (a_|_ v b))
18	17	ran 71	. . . . . . 7 (a_|_ ^ b) = (((a_|_ v b_|_) ^ (a_|_ v b)) ^ b)
19		anass 69	. . . . . . 7 (((a_|_ v b_|_) ^ (a_|_ v b)) ^ b) = ((a_|_ v b_|_) ^ ((a_|_ v b) ^ b))
20	18, 19	ax-r2 35	. . . . . 6 (a_|_ ^ b) = ((a_|_ v b_|_) ^ ((a_|_ v b) ^ b))
21	10	con2 64	. . . . . . 7 (a ^ b)_|_ = (a_|_ v b_|_)
22	21	ran 71	. . . . . 6 ((a ^ b)_|_ ^ b) = ((a_|_ v b_|_) ^ b)
23	7, 20, 22	3tr1 60	. . . . 5 (a_|_ ^ b) = ((a ^ b)_|_ ^ b)
24	23	lor 66	. . . 4 ((a ^ b) v (a_|_ ^ b)) = ((a ^ b) v ((a ^ b)_|_ ^ b))
25	24	ax-r1 34	. . 3 ((a ^ b) v ((a ^ b)_|_ ^ b)) = ((a ^ b) v (a_|_ ^ b))
26		ax-a2 30	. . . . . 6 ((a ^ b) v b) = (b v (a ^ b))
27		ancom 68	. . . . . . . 8 (a ^ b) = (b ^ a)
28	27	lor 66	. . . . . . 7 (b v (a ^ b)) = (b v (b ^ a))
29		a5b 112	. . . . . . 7 (b v (b ^ a)) = b
30	28, 29	ax-r2 35	. . . . . 6 (b v (a ^ b)) = b
31	26, 30	ax-r2 35	. . . . 5 ((a ^ b) v b) = b
32	31	df-le1 122	. . . 4 (a ^ b) =< b
33	32	oml2 433	. . 3 ((a ^ b) v ((a ^ b)_|_ ^ b)) = b
34		ancom 68	. . . 4 (a_|_ ^ b) = (b ^ a_|_)
35	27, 34	2or 67	. . 3 ((a ^ b) v (a_|_ ^ b)) = ((b ^ a) v (b ^ a_|_))
36	25, 33, 35	3tr2 61	. 2 b = ((b ^ a) v (b ^ a_|_))
37	36	df-c1 124	1 b C a

Syntax hints:   C wc 3  _|_wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  comcom3 436  com3ii 439  comor1 443  comorr2 445  comanr1 446  comanr2 447  fh2 452  com2or 465  nbdi 468  oml4 469  gsth 471  gsth2 472  gt1 474  i3bi 478  df2i3 480  i3lem1 486  comi31 490  lem4 493  i3abs3 506  i3con 533  ud1lem1 542  ud1lem3 544  ud2lem3 547  ud3lem1a 548  ud3lem1c 550  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1 563  ud4lem3 567  ud5lem1a 568  ud5lem1 571  u4lemaa 585  u4lemana 590  u3lemab 594  u3lemanb 599  comi12 689  i1com 690  comi1 691  u4lemle2 700  u5lembi 707  u12lembi 708  u1lem1 716  u3lem1 718  u5lem1 720  u3lem2 728  u4lem2 729  u5lem2 730  u4lem4 741  u5lem5 747  u5lem6 751  u1lem8 758  u1lem11 762  u3lem13b 772  u3lem15 777  bi1o1a 780  test 784  3vcom 795  3vded21 799  3vded3 801  2oalem1 807  bi3 821  bi4 822  orbi 824  negantlem2 831  elimcons 850  comanblem1 852  mhlem 858  mhlem1 859  marsdenlem1 862  marsdenlem2 863  marsdenlem3 864  mh2 866  mlaconjolem 867  mhcor1 870  govar 876  oau 909  oa23 916  oacom 991  oacom3 993

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org