Axiom ax-his3 5047

Description: Associative law for inner product. Postulate (S3) of [Beran] p. 95.

Assertion

Ref	Expression
ax-his3	|- ((A e. CC /\ B e. H~ /\ C e. H~) -> ((A .s B) .i C) = (A x. (B .i C)))

Detailed syntax breakdown of Axiom ax-his3

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cc 4026	. . . 4 class CC
3	1, 2	wcel 1092	. . 3 wff A e. CC
4		cB	. . . 4 class B
5		chil 4958	. . . 4 class H~
6	4, 5	wcel 1092	. . 3 wff B e. H~
7		cC	. . . 4 class C
8	7, 5	wcel 1092	. . 3 wff C e. H~
9	3, 6, 8	w3a 581	. 2 wff (A e. CC /\ B e. H~ /\ C e. H~)
10		csm 4960	. . . . 5 class .s
11	1, 4, 10	co 3001	. . . 4 class (A .s B)
12		csp 4963	. . . 4 class .i
13	11, 7, 12	co 3001	. . 3 class ((A .s B) .i C)
14	4, 7, 12	co 3001	. . . 4 class (B .i C)
15		cmulc 4032	. . . 4 class x.
16	1, 14, 15	co 3001	. . 3 class (A x. (B .i C))
17	13, 16	wceq 1091	. 2 wff ((A .s B) .i C) = (A x. (B .i C))
18	9, 17	wi 2	1 wff ((A e. CC /\ B e. H~ /\ C e. H~) -> ((A .s B) .i C) = (A x. (B .i C)))

This axiom is referenced by:  his5 5050  his2subt 5052  hizer1t 5054  normlem0 5062  normlem8 5071  bcseq 5073  norm-iii 5087  ocsh 5164  occllem1 5180  h1de2 5458

metamath.org