Metamath Proof Explorer


Theorem normlem7tALT

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 11-Oct-1999) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses normlem7t.1 A
normlem7t.2 B
Assertion normlem7tALT SS=1SAihB+SBihA2BihBAihA

Proof

Step Hyp Ref Expression
1 normlem7t.1 A
2 normlem7t.2 B
3 fveq2 S=ifSS=1S1S=ifSS=1S1
4 3 oveq1d S=ifSS=1S1SAihB=ifSS=1S1AihB
5 oveq1 S=ifSS=1S1SBihA=ifSS=1S1BihA
6 4 5 oveq12d S=ifSS=1S1SAihB+SBihA=ifSS=1S1AihB+ifSS=1S1BihA
7 6 breq1d S=ifSS=1S1SAihB+SBihA2BihBAihAifSS=1S1AihB+ifSS=1S1BihA2BihBAihA
8 eleq1 S=ifSS=1S1SifSS=1S1
9 fveq2 S=ifSS=1S1S=ifSS=1S1
10 9 eqeq1d S=ifSS=1S1S=1ifSS=1S1=1
11 8 10 anbi12d S=ifSS=1S1SS=1ifSS=1S1ifSS=1S1=1
12 eleq1 1=ifSS=1S11ifSS=1S1
13 fveq2 1=ifSS=1S11=ifSS=1S1
14 13 eqeq1d 1=ifSS=1S11=1ifSS=1S1=1
15 12 14 anbi12d 1=ifSS=1S111=1ifSS=1S1ifSS=1S1=1
16 ax-1cn 1
17 abs1 1=1
18 16 17 pm3.2i 11=1
19 11 15 18 elimhyp ifSS=1S1ifSS=1S1=1
20 19 simpli ifSS=1S1
21 19 simpri ifSS=1S1=1
22 20 1 2 21 normlem7 ifSS=1S1AihB+ifSS=1S1BihA2BihBAihA
23 7 22 dedth SS=1SAihB+SBihA2BihBAihA