Theorem comcom 453

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 31	. . . . . . . . . 10 (a' v b) = (b v a')
2	1	ran 78	. . . . . . . . 9 ((a' v b) ^ b) = ((b v a') ^ b)
3		ancom 74	. . . . . . . . 9 ((b v a') ^ b) = (b ^ (b v a'))
4	2, 3	ax-r2 36	. . . . . . . 8 ((a' v b) ^ b) = (b ^ (b v a'))
5		a5c 121	. . . . . . . 8 (b ^ (b v a')) = b
6	4, 5	ax-r2 36	. . . . . . 7 ((a' v b) ^ b) = b
7	6	lan 77	. . . . . 6 ((a' v b') ^ ((a' v b) ^ b)) = ((a' v b') ^ b)
8		comcom.1	. . . . . . . . . . . 12 a C b
9	8	df-c2 133	. . . . . . . . . . 11 a = ((a ^ b) v (a ^ b'))
10		df-a 40	. . . . . . . . . . . 12 (a ^ b) = (a' v b')'
11		anor1 88	. . . . . . . . . . . 12 (a ^ b') = (a' v b)'
12	10, 11	2or 72	. . . . . . . . . . 11 ((a ^ b) v (a ^ b')) = ((a' v b')' v (a' v b)')
13	9, 12	ax-r2 36	. . . . . . . . . 10 a = ((a' v b')' v (a' v b)')
14	13	ax-r4 37	. . . . . . . . 9 a' = ((a' v b')' v (a' v b)')'
15		df-a 40	. . . . . . . . . 10 ((a' v b') ^ (a' v b)) = ((a' v b')' v (a' v b)')'
16	15	ax-r1 35	. . . . . . . . 9 ((a' v b')' v (a' v b)')' = ((a' v b') ^ (a' v b))
17	14, 16	ax-r2 36	. . . . . . . 8 a' = ((a' v b') ^ (a' v b))
18	17	ran 78	. . . . . . 7 (a' ^ b) = (((a' v b') ^ (a' v b)) ^ b)
19		anass 76	. . . . . . 7 (((a' v b') ^ (a' v b)) ^ b) = ((a' v b') ^ ((a' v b) ^ b))
20	18, 19	ax-r2 36	. . . . . 6 (a' ^ b) = ((a' v b') ^ ((a' v b) ^ b))
21	10	con2 67	. . . . . . 7 (a ^ b)' = (a' v b')
22	21	ran 78	. . . . . 6 ((a ^ b)' ^ b) = ((a' v b') ^ b)
23	7, 20, 22	3tr1 63	. . . . 5 (a' ^ b) = ((a ^ b)' ^ b)
24	23	lor 70	. . . 4 ((a ^ b) v (a' ^ b)) = ((a ^ b) v ((a ^ b)' ^ b))
25	24	ax-r1 35	. . 3 ((a ^ b) v ((a ^ b)' ^ b)) = ((a ^ b) v (a' ^ b))
26		ax-a2 31	. . . . . 6 ((a ^ b) v b) = (b v (a ^ b))
27		ancom 74	. . . . . . . 8 (a ^ b) = (b ^ a)
28	27	lor 70	. . . . . . 7 (b v (a ^ b)) = (b v (b ^ a))
29		a5b 120	. . . . . . 7 (b v (b ^ a)) = b
30	28, 29	ax-r2 36	. . . . . 6 (b v (a ^ b)) = b
31	26, 30	ax-r2 36	. . . . 5 ((a ^ b) v b) = b
32	31	df-le1 130	. . . 4 (a ^ b) =< b
33	32	oml2 451	. . 3 ((a ^ b) v ((a ^ b)' ^ b)) = b
34		ancom 74	. . . 4 (a' ^ b) = (b ^ a')
35	27, 34	2or 72	. . 3 ((a ^ b) v (a' ^ b)) = ((b ^ a) v (b ^ a'))
36	25, 33, 35	3tr2 64	. 2 b = ((b ^ a) v (b ^ a'))
37	36	df-c1 132	1 b C a

Syntax hints:   C wc 3  'wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  comcom3 454  com3ii 457  comor1 461  comorr2 463  comanr1 464  comanr2 465  fh2 470  com2or 483  nbdi 486  oml4 487  gsth 489  gsth2 490  gt1 492  i3bi 496  df2i3 498  i3lem1 504  comi31 508  lem4 511  i3abs3 524  i3con 551  ud1lem1 560  ud1lem3 562  ud2lem3 565  ud3lem1a 566  ud3lem1c 568  ud3lem3 576  ud4lem1a 577  ud4lem1b 578  ud4lem1c 579  ud4lem1 581  ud4lem3 585  ud5lem1a 586  ud5lem1 589  u4lemaa 603  u4lemana 608  u3lemab 612  u3lemanb 617  comi12 707  i1com 708  comi1 709  u4lemle2 718  u5lembi 725  u12lembi 726  u1lem1 734  u3lem1 736  u5lem1 738  u3lem2 746  u4lem2 747  u5lem2 748  u4lem4 759  u5lem5 765  u5lem6 769  u1lem8 776  u1lem11 780  u3lem13b 790  u3lem15 795  bi1o1a 798  test 802  3vcom 813  3vded21 817  3vded3 819  2oalem1 825  bi3 839  bi4 840  orbi 842  negantlem2 849  elimcons 868  comanblem1 870  mhlem 876  mhlem1 877  marsdenlem1 880  marsdenlem2 881  marsdenlem3 882  mh2 884  mlaconjolem 885  mhcor1 888  e2ast2 894  e2astlem1 895  govar 896  oau 929  oa23 936  oacom 1011  oacom3 1013  lem4.6.2e1 1079  lem4.6.6i1j3 1091

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

Copyright terms: Public domain