Metamath Proof Explorer


Theorem mdsymlem2

Description: Lemma for mdsymi . (Contributed by NM, 1-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdsymlem1.1 AC
mdsymlem1.2 BC
mdsymlem1.3 C=Ap
Assertion mdsymlem2 pHAtomsBCAB𝑀*ApABB0rHAtomsqHAtomspqrqArB

Proof

Step Hyp Ref Expression
1 mdsymlem1.1 AC
2 mdsymlem1.2 BC
3 mdsymlem1.3 C=Ap
4 2 hatomici B0rHAtomsrB
5 simplll pHAtomsBCAB𝑀*ApABrHAtomsrBpHAtoms
6 atelch pHAtomspC
7 atelch rHAtomsrC
8 chub1 pCrCppr
9 6 7 8 syl2an pHAtomsrHAtomsppr
10 9 adantlr pHAtomsBCArHAtomsppr
11 10 adantlr pHAtomsBCAB𝑀*ApABrHAtomsppr
12 1 2 3 mdsymlem1 pCBCAB𝑀*ApABpA
13 6 12 sylanl1 pHAtomsBCAB𝑀*ApABpA
14 13 adantr pHAtomsBCAB𝑀*ApABrHAtomspA
15 11 14 jca pHAtomsBCAB𝑀*ApABrHAtomspprpA
16 15 anim1i pHAtomsBCAB𝑀*ApABrHAtomsrBpprpArB
17 anass pprpArBpprpArB
18 16 17 sylib pHAtomsBCAB𝑀*ApABrHAtomsrBpprpArB
19 18 anasss pHAtomsBCAB𝑀*ApABrHAtomsrBpprpArB
20 oveq1 q=pqr=pr
21 20 sseq2d q=ppqrppr
22 sseq1 q=pqApA
23 22 anbi1d q=pqArBpArB
24 21 23 anbi12d q=ppqrqArBpprpArB
25 24 rspcev pHAtomspprpArBqHAtomspqrqArB
26 5 19 25 syl2anc pHAtomsBCAB𝑀*ApABrHAtomsrBqHAtomspqrqArB
27 26 exp32 pHAtomsBCAB𝑀*ApABrHAtomsrBqHAtomspqrqArB
28 27 reximdvai pHAtomsBCAB𝑀*ApABrHAtomsrBrHAtomsqHAtomspqrqArB
29 4 28 syl5 pHAtomsBCAB𝑀*ApABB0rHAtomsqHAtomspqrqArB