Theorem comcom5 458

Description: Commutation equivalence. Kalmbach 83 p. 23.

Hypothesis

Ref	Expression
comcom5.1	a⊥ C b⊥

Assertion

Ref	Expression
comcom5	a C b

Proof of Theorem comcom5

Step	Hyp	Ref	Expression
1		comcom5.1	. . . . 5 a⊥ C b⊥
2	1	comcom4 455	. . . 4 a⊥ ⊥ C b⊥ ⊥
3	2	df-c2 133	. . 3 a⊥ ⊥ = ((a⊥ ⊥ ∩ b⊥ ⊥ ) ∪ (a⊥ ⊥ ∩ b⊥ ⊥ ⊥ ))
4		ax-a1 30	. . 3 a = a⊥ ⊥
5		ax-a1 30	. . . . 5 b = b⊥ ⊥
6	4, 5	2an 79	. . . 4 (a ∩ b) = (a⊥ ⊥ ∩ b⊥ ⊥ )
7		ax-a1 30	. . . . 5 b⊥ = b⊥ ⊥ ⊥
8	4, 7	2an 79	. . . 4 (a ∩ b⊥ ) = (a⊥ ⊥ ∩ b⊥ ⊥ ⊥ )
9	6, 8	2or 72	. . 3 ((a ∩ b) ∪ (a ∩ b⊥ )) = ((a⊥ ⊥ ∩ b⊥ ⊥ ) ∪ (a⊥ ⊥ ∩ b⊥ ⊥ ⊥ ))
10	3, 4, 9	3tr1 63	. 2 a = ((a ∩ b) ∪ (a ∩ b⊥ ))
11	10	df-c1 132	1 a C b

Syntax hints:   C wc 3  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

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

This theorem is referenced by:  comcom6  459  comcom7  460  comdr  466  df2c1  468  com2an  484  oml4  487  gstho  491  df2i3  498  i3lem2  505  comi31  508  ud1lem1  560  ud1lem3  562  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1d  580  ud4lem1  581  ud5lem1a  586