let L be non empty join-commutative join-associative Huntington ComplLLattStr ; for a, b, c being Element of L holds (a *' (b + c)) ` = (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))
let a, b, c be Element of L; (a *' (b + c)) ` = (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))
set D = (a *' (b `)) *' (c `);
set E = ((a `) *' b) *' c;
set F = ((a `) *' b) *' (c `);
set G = ((a `) *' (b `)) *' c;
set H = ((a `) *' (b `)) *' (c `);
A1: a ` =
((a `) *' b) + ((a `) *' (b `))
by Def6
.=
((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + ((a `) *' (b `))
by Def6
.=
((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `)))
by Def6
;
A2: (b `) *' (c `) =
(a *' ((b `) *' (c `))) + ((a `) *' ((b `) *' (c `)))
by Th1
.=
((a *' (b `)) *' (c `)) + ((a `) *' ((b `) *' (c `)))
by Th16
.=
((a *' (b `)) *' (c `)) + (((a `) *' (b `)) *' (c `))
by Th16
;
(a *' (b + c)) ` =
(a `) + ((b + c) `)
by Th3
.=
(a `) + ((((b `) *' (c `)) `) `)
by Th17
.=
(a `) + ((b `) *' (c `))
by Th3
;
hence (a *' (b + c)) ` =
((((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `)))) + (((a `) *' (b `)) *' (c `))) + ((a *' (b `)) *' (c `))
by A1, A2, LATTICES:def 5
.=
(((((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))) + (((a `) *' (b `)) *' (c `))) + ((a *' (b `)) *' (c `))
by LATTICES:def 5
.=
((((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + ((((a `) *' (b `)) *' (c `)) + (((a `) *' (b `)) *' (c `)))) + ((a *' (b `)) *' (c `))
by LATTICES:def 5
.=
((((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))) + ((a *' (b `)) *' (c `))
by Def7
.=
((a *' (b `)) *' (c `)) + (((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `))))
by LATTICES:def 5
.=
(((a *' (b `)) *' (c `)) + ((((a `) *' b) *' c) + (((a `) *' b) *' (c `)))) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `)))
by LATTICES:def 5
.=
((((a *' (b `)) *' (c `)) + ((((a `) *' b) *' c) + (((a `) *' b) *' (c `)))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))
by LATTICES:def 5
.=
(((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))
by LATTICES:def 5
;
verum